diff --git a/.github/workflows/c-verifier-tests.yml b/.github/workflows/c-verifier-tests.yml new file mode 100644 index 0000000000..8e2ec09915 --- /dev/null +++ b/.github/workflows/c-verifier-tests.yml @@ -0,0 +1,73 @@ +name: Uclid5-based Verifier Tests + +on: + # Trigger this workflow also on workflow_call events. + workflow_call: + inputs: + compiler-ref: + required: false + type: string + runtime-ref: + required: false + type: string + +jobs: + run: + strategy: + matrix: + platform: [ubuntu-latest] + runs-on: ${{ matrix.platform }} + steps: + - name: Check out lingua-franca repository + uses: actions/checkout@v3 + with: + repository: lf-lang/lingua-franca + submodules: true + ref: ${{ inputs.compiler-ref }} + fetch-depth: 0 + - name: Prepare build environment + uses: ./.github/actions/prepare-build-env + - name: Check out specific ref of reactor-c + uses: actions/checkout@v3 + with: + repository: lf-lang/reactor-c + path: core/src/main/resources/lib/c/reactor-c + ref: ${{ inputs.runtime-ref }} + if: ${{ inputs.runtime-ref }} + - name: Check out Uclid5 repository + uses: actions/checkout@v3 + with: + repository: uclid-org/uclid + ref: 4fd5e566c5f87b052f92e9b23723a85e1c4d8c1c + path: uclid + - name: Download Z3 + working-directory: uclid/ + if: steps.cache-z3.outputs.cache-hit != 'true' + run: ./get-z3-linux.sh + - name: Add Z3 to Path + working-directory: uclid/ + run: | + echo "$(pwd)/z3/bin/" >> $GITHUB_PATH + echo "LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$(pwd)/z3/bin/" >> $GITHUB_ENV + - name: Print Z3 Version + run: z3 --version + - name: Install Uclid5 + working-directory: uclid/ + run: | + sbt update clean compile + sbt universal:packageBin + cd target/universal/ + unzip uclid-0.9.5.zip + ./uclid-0.9.5/bin/uclid --help + echo "$(pwd)/uclid-0.9.5/bin" >> $GITHUB_PATH + cd ../.. + - name: Run verifier tests + run: | + echo "$pwd" + ls -la + ./gradlew core:integrationTest --tests org.lflang.tests.runtime.CVerifierTest.* core:integrationTestCodeCoverageReport + - name: Report to CodeCov + uses: ./.github/actions/report-code-coverage + with: + files: core/build/reports/jacoco/integrationTestCodeCoverageReport/integrationTestCodeCoverageReport.xml + if: ${{ github.repository == 'lf-lang/lingua-franca' }} diff --git a/.github/workflows/only-c.yml b/.github/workflows/only-c.yml index 9b457b6d01..ae9016465c 100644 --- a/.github/workflows/only-c.yml +++ b/.github/workflows/only-c.yml @@ -41,3 +41,7 @@ jobs: with: use-cpp: true all-platforms: ${{ !github.event.pull_request.draft }} + + # Run the Uclid-based LF Verifier benchmarks. + verifier: + uses: ./.github/workflows/c-verifier-tests.yml diff --git a/.gitignore b/.gitignore index 313beb67da..35ccb1f2f9 100644 --- a/.gitignore +++ b/.gitignore @@ -155,6 +155,10 @@ gradle-app.setting ### Gradle Patch ### **/build/ +### Antlr 4 ### +**/.antlr/ +**/generated/ + # End of https://www.toptal.com/developers/gitignore/api/intellij,gradle,eclipse,maven,visualstudiocode ### xtext artifaccts diff --git a/buildSrc/src/main/groovy/org.lflang.antlr-conventions.gradle b/buildSrc/src/main/groovy/org.lflang.antlr-conventions.gradle new file mode 100644 index 0000000000..096e0636b3 --- /dev/null +++ b/buildSrc/src/main/groovy/org.lflang.antlr-conventions.gradle @@ -0,0 +1,16 @@ +plugins { + id 'antlr' +} + +repositories { + mavenCentral() +} + +dependencies { + antlr "org.antlr:antlr4:${antlrVersion}" +} + +if (project.tasks.findByName('compileKotlin')) { + // make all kotlin compile tasks dependent on the antl generation tasks + tasks.withType(org.jetbrains.kotlin.gradle.tasks.KotlinCompile).each(it -> it.dependsOn(tasks.withType(AntlrTask))) +} diff --git a/buildSrc/src/main/groovy/org.lflang.java-conventions.gradle b/buildSrc/src/main/groovy/org.lflang.java-conventions.gradle index 5165d03fa6..9fc4fa50f9 100644 --- a/buildSrc/src/main/groovy/org.lflang.java-conventions.gradle +++ b/buildSrc/src/main/groovy/org.lflang.java-conventions.gradle @@ -10,7 +10,7 @@ repositories { spotless { java { - targetExclude 'src-gen/**', 'test-gen/**' + targetExclude 'src-gen/**', 'test-gen/**', 'build/**' // The following is quoted from https://github.com/google/google-java-format // "Note: There is no configurability as to the formatter's algorithm for formatting. // This is a deliberate design decision to unify our code formatting on a single format." diff --git a/cli/lfc/src/main/java/org/lflang/cli/Lfc.java b/cli/lfc/src/main/java/org/lflang/cli/Lfc.java index dd2d6fe9d2..f8a51d367f 100644 --- a/cli/lfc/src/main/java/org/lflang/cli/Lfc.java +++ b/cli/lfc/src/main/java/org/lflang/cli/Lfc.java @@ -79,6 +79,12 @@ public class Lfc extends CliBase { description = "Do not invoke target compiler.") private boolean noCompile; + @Option( + names = {"--verify"}, + arity = "0", + description = "Run the generated verification models.") + private boolean verify; + @Option( names = {"--print-statistics"}, arity = "0", @@ -250,6 +256,10 @@ public Properties getGeneratorArgs() { props.setProperty(BuildParm.NO_COMPILE.getKey(), "true"); } + if (verify) { + props.setProperty(BuildParm.VERIFY.getKey(), "true"); + } + if (targetCompiler != null) { props.setProperty(BuildParm.TARGET_COMPILER.getKey(), targetCompiler); } diff --git a/core/build.gradle b/core/build.gradle index 0d87a3e729..23b412b6a8 100644 --- a/core/build.gradle +++ b/core/build.gradle @@ -1,6 +1,7 @@ plugins { id 'org.lflang.java-library-conventions' id 'org.lflang.kotlin-conventions' + id 'org.lflang.antlr-conventions' } sourceSets { @@ -34,6 +35,8 @@ dependencies { exclude group: 'de.cau.cs.kieler.swt.mock' } + implementation "org.json:json:$jsonVersion" + testImplementation "org.junit.jupiter:junit-jupiter-api:$jupiterVersion" testImplementation "org.junit.jupiter:junit-jupiter-engine:$jupiterVersion" testImplementation "org.junit.platform:junit-platform-commons:$jUnitPlatformVersion" @@ -73,6 +76,12 @@ clean.dependsOn(cleanGenerateXtextLanguage) spotlessJava.mustRunAfter(generateXtextLanguage) rootProject.spotlessMisc.mustRunAfter(generateXtextLanguage) + +// antlr4 configuration +generateGrammarSource { + arguments += ['-visitor', '-package', 'org.lflang.dsl'] +} + tasks.register('getSubmoduleVersions', Exec) { description('Run a Git command to get the current status of submodules') workingDir project.rootDir diff --git a/core/src/integrationTest/java/org/lflang/tests/runtime/CCppTest.java b/core/src/integrationTest/java/org/lflang/tests/runtime/CCppTest.java index 3142058c23..6324098963 100644 --- a/core/src/integrationTest/java/org/lflang/tests/runtime/CCppTest.java +++ b/core/src/integrationTest/java/org/lflang/tests/runtime/CCppTest.java @@ -46,6 +46,7 @@ private static boolean isExcludedFromCCpp(TestCategory category) { excluded |= category == TestCategory.ZEPHYR_THREADED; excluded |= category == TestCategory.ARDUINO; excluded |= category == TestCategory.NO_INLINING; + excluded |= category == TestCategory.VERIFIER; return !excluded; } } diff --git a/core/src/integrationTest/java/org/lflang/tests/runtime/CVerifierTest.java b/core/src/integrationTest/java/org/lflang/tests/runtime/CVerifierTest.java new file mode 100644 index 0000000000..d9bde8b3ed --- /dev/null +++ b/core/src/integrationTest/java/org/lflang/tests/runtime/CVerifierTest.java @@ -0,0 +1,30 @@ +package org.lflang.tests.runtime; + +import java.util.List; +import org.junit.jupiter.api.Assumptions; +import org.junit.jupiter.api.Test; +import org.lflang.Target; +import org.lflang.tests.TestBase; +import org.lflang.tests.TestRegistry; + +public class CVerifierTest extends TestBase { + protected CVerifierTest() { + super(Target.C); + } + + @Test + public void runVerifierTests() { + Assumptions.assumeTrue(isLinux() || isMac(), "Verifier tests only run on Linux or macOS"); + + super.runTestsFor( + List.of(Target.C), + Message.DESC_VERIFIER, + TestRegistry.TestCategory.VERIFIER::equals, + test -> { + test.getContext().getTargetConfig().verify = true; + return true; + }, + TestLevel.BUILD, + false); + } +} diff --git a/core/src/main/antlr/C.g4 b/core/src/main/antlr/C.g4 new file mode 100644 index 0000000000..2fd6c3aedf --- /dev/null +++ b/core/src/main/antlr/C.g4 @@ -0,0 +1,908 @@ +/* + [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 + | Constant + | StringLiteral+ + | '(' expression ')' + | genericSelection + | '__extension__'? '(' compoundStatement ')' // Blocks (GCC extension) + | '__builtin_va_arg' '(' unaryExpression ',' typeName ')' + | '__builtin_offsetof' '(' typeName ',' unaryExpression ')' + ; + +genericSelection + : '_Generic' '(' assignmentExpression ',' genericAssocList ')' + ; + +genericAssocList + : genericAssociation (',' genericAssociation)* + ; + +genericAssociation + : (typeName | 'default') ':' assignmentExpression + ; + +postfixExpression + : + ( primaryExpression + | '__extension__'? '(' typeName ')' '{' initializerList ','? '}' + ) + ('[' expression ']' + | '(' argumentExpressionList? ')' + | ('.' | '->') Identifier + | ('++' | '--') + )* + ; + +argumentExpressionList + : assignmentExpression (',' assignmentExpression)* + ; + +unaryExpression + : + ('++' | '--' | 'sizeof')* + (postfixExpression + | unaryOperator castExpression + | ('sizeof' | '_Alignof') '(' typeName ')' + | '&&' Identifier // GCC extension address of label + ) + ; + +unaryOperator + : '&' | '*' | '+' | '-' | '~' | '!' + ; + +castExpression + : '__extension__'? '(' typeName ')' castExpression + | unaryExpression + | DigitSequence // for + ; + +multiplicativeExpression + : castExpression (('*'|'/'|'%') castExpression)* + ; + +additiveExpression + : multiplicativeExpression (('+'|'-') multiplicativeExpression)* + ; + +shiftExpression + : additiveExpression (('<<'|'>>') additiveExpression)* + ; + +relationalExpression + : shiftExpression (('<'|'>'|'<='|'>=') shiftExpression)* + ; + +equalityExpression + : relationalExpression (('=='| '!=') relationalExpression)* + ; + +andExpression + : equalityExpression ( '&' equalityExpression)* + ; + +exclusiveOrExpression + : andExpression ('^' andExpression)* + ; + +inclusiveOrExpression + : exclusiveOrExpression ('|' exclusiveOrExpression)* + ; + +logicalAndExpression + : inclusiveOrExpression ('&&' inclusiveOrExpression)* + ; + +logicalOrExpression + : logicalAndExpression ( '||' logicalAndExpression)* + ; + +conditionalExpression + : logicalOrExpression ('?' expression ':' conditionalExpression)? + ; + +assignmentExpression + : conditionalExpression + | unaryExpression assignmentOperator assignmentExpression + | DigitSequence // for + ; + +assignmentOperator + : '=' | '*=' | '/=' | '%=' | '+=' | '-=' | '<<=' | '>>=' | '&=' | '^=' | '|=' + ; + +expression + : assignmentExpression (',' assignmentExpression)* + ; + +constantExpression + : conditionalExpression + ; + +declaration + : declarationSpecifiers initDeclaratorList? ';' + | staticAssertDeclaration + ; + +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' + | 'float' + | 'double' + | 'signed' + | 'unsigned' + | '_Bool' + | '_Complex' + | '__m128' + | '__m128d' + | '__m128i') + | '__extension__' '(' ('__m128' | '__m128d' | '__m128i') ')' + | atomicTypeSpecifier + | structOrUnionSpecifier + | enumSpecifier + | typedefName + | '__typeof__' '(' constantExpression ')' // GCC extension + ; + +structOrUnionSpecifier + : structOrUnion Identifier? '{' structDeclarationList '}' + | structOrUnion Identifier + ; + +structOrUnion + : 'struct' + | 'union' + ; + +structDeclarationList + : structDeclaration+ + ; + +structDeclaration // The first two rules have priority order and cannot be simplified to one expression. + : specifierQualifierList structDeclaratorList ';' + | specifierQualifierList ';' + | staticAssertDeclaration + ; + +specifierQualifierList + : (typeSpecifier| typeQualifier) specifierQualifierList? + ; + +structDeclaratorList + : structDeclarator (',' structDeclarator)* + ; + +structDeclarator + : declarator + | declarator? ':' constantExpression + ; + +enumSpecifier + : 'enum' Identifier? '{' enumeratorList ','? '}' + | 'enum' Identifier + ; + +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 + | '(' declarator ')' + | directDeclarator '[' typeQualifierList? assignmentExpression? ']' + | directDeclarator '[' 'static' typeQualifierList? assignmentExpression ']' + | directDeclarator '[' typeQualifierList 'static' assignmentExpression ']' + | directDeclarator '[' typeQualifierList? '*' ']' + | directDeclarator '(' parameterTypeList ')' + | directDeclarator '(' identifierList? ')' + | Identifier ':' DigitSequence // bit field + | vcSpecificModifer Identifier // Visual C Extension + | '(' vcSpecificModifer declarator ')' // Visual C Extension + ; + +vcSpecificModifer + : ('__cdecl' + | '__clrcall' + | '__stdcall' + | '__fastcall' + | '__thiscall' + | '__vectorcall') + ; + + +gccDeclaratorExtension + : '__asm' '(' StringLiteral+ ')' + | gccAttributeSpecifier + ; + +gccAttributeSpecifier + : '__attribute__' '(' '(' gccAttributeList ')' ')' + ; + +gccAttributeList + : gccAttribute? (',' gccAttribute?)* + ; + +gccAttribute + : ~(',' | '(' | ')') // relaxed def for "identifier or reserved word" + ('(' argumentExpressionList? ')')? + ; + +nestedParenthesesBlock + : ( ~('(' | ')') + | '(' nestedParenthesesBlock ')' + )* + ; + +pointer + : (('*'|'^') typeQualifierList?)+ // ^ - Blocks language extension + ; + +typeQualifierList + : typeQualifier+ + ; + +parameterTypeList + : parameterList (',' '...')? + ; + +parameterList + : parameterDeclaration (',' parameterDeclaration)* + ; + +parameterDeclaration + : declarationSpecifiers declarator + | declarationSpecifiers2 abstractDeclarator? + ; + +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? initializer (',' designation? 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 + | 'case' constantExpression ':' statement + | 'default' ':' statement + ; + +compoundStatement + : '{' blockItemList? '}' + ; + +blockItemList + : blockItem+ + ; + +// Reaction body is a blockItem. +blockItem + : statement + | declaration + ; + +expressionStatement + : expression? ';' + ; + +selectionStatement + : 'if' '(' expression ')' statement ('else' statement)? + | 'switch' '(' expression ')' statement + ; + +iterationStatement + : While '(' expression ')' statement + | Do statement While '(' expression ')' ';' + | For '(' forCondition ')' statement + ; + +// | 'for' '(' expression? ';' expression? ';' forUpdate? ')' statement +// | For '(' declaration expression? ';' expression? ')' statement + +forCondition + : (forDeclaration | expression?) ';' forExpression? ';' forExpression? + ; + +forDeclaration + : declarationSpecifiers initDeclaratorList? + ; + +forExpression + : assignmentExpression (',' assignmentExpression)* + ; + +jumpStatement + : ('goto' Identifier + | ('continue'| 'break') + | 'return' expression? + | 'goto' unaryExpression // GCC extension + ) + ';' + ; + +compilationUnit + : translationUnit? EOF + ; + +translationUnit + : externalDeclaration+ + ; + +externalDeclaration + : functionDefinition + | declaration + | ';' // stray ; + ; + +functionDefinition + : declarationSpecifiers? declarator declarationList? compoundStatement + ; + +declarationList + : declaration+ + ; + +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 + ; \ No newline at end of file diff --git a/core/src/main/antlr/MTLLexer.g4 b/core/src/main/antlr/MTLLexer.g4 new file mode 100644 index 0000000000..5d0b803ff8 --- /dev/null +++ b/core/src/main/antlr/MTLLexer.g4 @@ -0,0 +1,117 @@ +lexer grammar MTLLexer; + +COMMA + : ',' + ; + +LPAREN + : '(' + ; + +RPAREN + : ')' + ; + +LBRACKET + : '[' + ; + +RBRACKET + : ']' + ; + +LAND + : '&&' + ; + +LOR + : '||' + ; + +EQUI + : '<==>' + ; + +IMPL + : '==>' + ; + +UNTIL + : 'U' + ; + +NEGATION + : '!' + ; + +NEXT + : 'X' + ; + +GLOBALLY + : 'G' + ; + +FINALLY + : 'F' + ; + +WS + : [ \t\r\n]+ -> skip + ; + +TRUE + : 'true' + ; + +FALSE + : 'false' + ; + +PLUS + : '+' + ; + +MINUS + : '-' + ; + +TIMES + : '*' + ; + +DIV + : '/' + ; + +EQ + : '==' + ; + +NEQ + : '!=' + ; + +LT + : '<' + ; + +LE + : '<=' + ; + +GT + : '>' + ; + +GE + : '>=' + ; + +INTEGER + : [0-9]+ + ; + +ID + : ([a-zA-Z0-9]|'_')+ + ; diff --git a/core/src/main/antlr/MTLParser.g4 b/core/src/main/antlr/MTLParser.g4 new file mode 100644 index 0000000000..1a5d39b9b4 --- /dev/null +++ b/core/src/main/antlr/MTLParser.g4 @@ -0,0 +1,82 @@ +parser grammar MTLParser; + +options { tokenVocab=MTLLexer; } + +mtl + : equivalence + ; + +equivalence + : left=implication ( EQUI right=implication )? + ; + +implication + : left=disjunction ( IMPL right=disjunction )? + ; + +disjunction + : terms+=conjunction ( LOR terms+=conjunction )* + ; + +conjunction + : terms+=binaryOp ( LAND terms+=binaryOp )* + ; + +binaryOp + : left=unaryOp ( UNTIL timeInterval=interval right=unaryOp )? # Until + ; + +unaryOp + : formula=primary # NoUnaryOp + | NEGATION formula=primary # Negation + | NEXT timeInterval=interval formula=primary # Next + | GLOBALLY timeInterval=interval formula=primary # Globally + | FINALLY timeInterval=interval formula=primary # Finally + ; + +primary + : atom=atomicProp + | id=ID + | LPAREN formula=mtl RPAREN + ; + +atomicProp + : primitive=TRUE + | primitive=FALSE + | left=expr op=relOp right=expr + ; + +interval + : (LPAREN|LBRACKET) lowerbound=time COMMA upperbound=time (RPAREN|RBRACKET) # Range + | LBRACKET instant=time RBRACKET # Singleton + ; + +time + : value=INTEGER (unit=ID)? + ; + +sum + : terms+=difference (PLUS terms+=difference)* + ; + +difference + : terms+=product (MINUS terms+=product)* + ; + +product + : terms+=quotient (TIMES terms+=quotient)* + ; + +quotient + : terms+=expr (DIV terms+=expr)* + ; + +relOp + : EQ | NEQ | LT | LE | GT | GE + ; + +expr + : ID + | LPAREN sum RPAREN + | INTEGER + ; diff --git a/core/src/main/java/org/lflang/FileConfig.java b/core/src/main/java/org/lflang/FileConfig.java index 831cb7957f..eb2d53c655 100644 --- a/core/src/main/java/org/lflang/FileConfig.java +++ b/core/src/main/java/org/lflang/FileConfig.java @@ -32,6 +32,9 @@ public abstract class FileConfig { /** Default name of the directory to store generated sources in. */ public static final String DEFAULT_SRC_GEN_DIR = "src-gen"; + /** Default name of the directory to store generated verification models in. */ + public static final String DEFAULT_MODEL_GEN_DIR = "mod-gen"; + // Public fields. /** The directory in which to put binaries, if the code generator produces any. */ @@ -93,6 +96,12 @@ public abstract class FileConfig { */ protected Path srcGenPath; + /** Path representation of the root directory for generated verification models. */ + protected Path modelGenBasePath; + + /** The directory in which to put the generated verification models. */ + protected Path modelGenPath; + // private fields /** @@ -133,6 +142,9 @@ public FileConfig(Resource resource, Path srcGenBasePath, boolean useHierarchica Path binRoot = outPath.resolve(DEFAULT_BIN_DIR); this.binPath = useHierarchicalBin ? binRoot.resolve(getSubPkgPath(srcPath)) : binRoot; + this.modelGenBasePath = outPath.resolve(DEFAULT_MODEL_GEN_DIR); + this.modelGenPath = modelGenBasePath.resolve(getSubPkgPath(srcPath)).resolve(name); + this.iResource = FileUtil.getIResource(resource); } @@ -214,6 +226,20 @@ protected Path getSubPkgPath(Path srcPath) { return relSrcPath; } + /** + * Path representation of the root directory for generated verification models. This is the root, + * meaning that if the source file is x/y/Z.lf relative to the package root, then the generated + * sources will be put in x/y/Z relative to this URI. + */ + public Path getModelGenBasePath() { + return modelGenBasePath; + } + + /** The directory in which to put the generated verification models. */ + public Path getModelGenPath() { + return modelGenPath; + } + /** * Clean any artifacts produced by the code generator and target compilers. * @@ -226,6 +252,7 @@ protected Path getSubPkgPath(Path srcPath) { public void doClean() throws IOException { FileUtil.deleteDirectory(binPath); FileUtil.deleteDirectory(srcGenBasePath); + FileUtil.deleteDirectory(modelGenBasePath); } private static Path getPkgPath(Resource resource) throws IOException { diff --git a/core/src/main/java/org/lflang/TargetConfig.java b/core/src/main/java/org/lflang/TargetConfig.java index 86ac029131..8f6a8cd5bd 100644 --- a/core/src/main/java/org/lflang/TargetConfig.java +++ b/core/src/main/java/org/lflang/TargetConfig.java @@ -82,6 +82,9 @@ public TargetConfig(Properties cliArgs, TargetDecl target, MessageReporter messa if (cliArgs.containsKey("no-compile")) { this.noCompile = true; } + if (cliArgs.containsKey("verify")) { + this.verify = true; + } if (cliArgs.containsKey("docker")) { var arg = cliArgs.getProperty("docker"); if (Boolean.parseBoolean(arg)) { @@ -229,6 +232,9 @@ public TargetConfig(Properties cliArgs, TargetDecl target, MessageReporter messa /** If true, do not perform runtime validation. The default is false. */ public boolean noRuntimeValidation = false; + /** If true, check the generated verification model. The default is false. */ + public boolean verify = false; + /** * Set the target platform config. This tells the build system what platform-specific support * files it needs to incorporate at compile time. diff --git a/core/src/main/java/org/lflang/TargetProperty.java b/core/src/main/java/org/lflang/TargetProperty.java index f86f87ea2b..aa091af3cd 100644 --- a/core/src/main/java/org/lflang/TargetProperty.java +++ b/core/src/main/java/org/lflang/TargetProperty.java @@ -410,6 +410,16 @@ public enum TargetProperty { config.noRuntimeValidation = ASTUtils.toBoolean(value); }), + /** Directive to check the generated verification model. */ + VERIFY( + "verify", + PrimitiveType.BOOLEAN, + Arrays.asList(Target.C), + (config) -> ASTUtils.toElement(config.verify), + (config, value, err) -> { + config.verify = ASTUtils.toBoolean(value); + }), + /** * Directive to specify the platform for cross code generation. This is either a string of the * platform or a dictionary of options that includes the string name. diff --git a/core/src/main/java/org/lflang/TimeValue.java b/core/src/main/java/org/lflang/TimeValue.java index f0bb94820c..899fe97aa8 100644 --- a/core/src/main/java/org/lflang/TimeValue.java +++ b/core/src/main/java/org/lflang/TimeValue.java @@ -137,6 +137,34 @@ public long toNanoSeconds() { return makeNanosecs(time, unit); } + /** Return a TimeValue based on a nanosecond value. */ + public static TimeValue fromNanoSeconds(long ns) { + if (ns == 0) return ZERO; + long time; + if ((time = ns / 604_800_016_558_522L) > 0 && ns % 604_800_016_558_522L == 0) { + return new TimeValue(time, TimeUnit.WEEK); + } + if ((time = ns / 86_400_000_000_000L) > 0 && ns % 86_400_000_000_000L == 0) { + return new TimeValue(time, TimeUnit.DAY); + } + if ((time = ns / 3_600_000_000_000L) > 0 && ns % 3_600_000_000_000L == 0) { + return new TimeValue(time, TimeUnit.HOUR); + } + if ((time = ns / 60_000_000_000L) > 0 && ns % 60_000_000_000L == 0) { + return new TimeValue(time, TimeUnit.MINUTE); + } + if ((time = ns / 1_000_000_000) > 0 && ns % 1_000_000_000 == 0) { + return new TimeValue(time, TimeUnit.SECOND); + } + if ((time = ns / 1_000_000) > 0 && ns % 1_000_000 == 0) { + return new TimeValue(time, TimeUnit.MILLI); + } + if ((time = ns / 1000) > 0 && ns % 1000 == 0) { + return new TimeValue(time, TimeUnit.MICRO); + } + return new TimeValue(ns, TimeUnit.NANO); + } + /** Return a string representation of this time value. */ public String toString() { return unit != null ? time + " " + unit.getCanonicalName() : Long.toString(time); diff --git a/core/src/main/java/org/lflang/analyses/c/AbstractAstVisitor.java b/core/src/main/java/org/lflang/analyses/c/AbstractAstVisitor.java new file mode 100644 index 0000000000..c279f962d6 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/AbstractAstVisitor.java @@ -0,0 +1,17 @@ +package org.lflang.analyses.c; + +import java.util.List; + +/** Modeled after {@link AbstractParseTreeVisitor}. */ +public abstract class AbstractAstVisitor implements AstVisitor { + + @Override + public T visit(CAst.AstNode tree) { + return tree.accept(this); + } + + @Override + public T visit(CAst.AstNode tree, List nodeList) { + return tree.accept(this, nodeList); + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/AstUtils.java b/core/src/main/java/org/lflang/analyses/c/AstUtils.java new file mode 100644 index 0000000000..c3ac49b6fd --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/AstUtils.java @@ -0,0 +1,78 @@ +package org.lflang.analyses.c; + +import java.util.List; +import org.antlr.v4.runtime.ParserRuleContext; +import org.antlr.v4.runtime.misc.Interval; + +public class AstUtils { + + public static CAst.AstNode takeConjunction(List conditions) { + if (conditions.size() == 0) { + return new CAst.LiteralNode("true"); + } else if (conditions.size() == 1) { + return conditions.get(0); + } else { + // Take the conjunction of all the conditions. + CAst.LogicalAndNode top = new CAst.LogicalAndNode(); + CAst.LogicalAndNode cur = top; + for (int i = 0; i < conditions.size() - 1; i++) { + cur.left = conditions.get(i); + if (i == conditions.size() - 2) { + cur.right = conditions.get(i + 1); + } else { + cur.right = new CAst.LogicalAndNode(); + cur = (CAst.LogicalAndNode) cur.right; + } + } + return top; + } + } + + public static CAst.AstNode takeDisjunction(List conditions) { + if (conditions.size() == 0) { + return new CAst.LiteralNode("true"); + } else if (conditions.size() == 1) { + return conditions.get(0); + } else { + // Take the disjunction of all the conditions. + CAst.LogicalOrNode top = new CAst.LogicalOrNode(); + CAst.LogicalOrNode cur = top; + for (int i = 0; i < conditions.size() - 1; i++) { + cur.left = conditions.get(i); + if (i == conditions.size() - 2) { + cur.right = conditions.get(i + 1); + } else { + cur.right = new CAst.LogicalOrNode(); + cur = (CAst.LogicalOrNode) cur.right; + } + } + return top; + } + } + + /** + * A handy function for debugging ASTs. It prints the stack trace of the visitor functions and + * shows the text matched by the ANTLR rules. + */ + public static void printStackTraceAndMatchedText(ParserRuleContext ctx) { + System.out.println("========== AST DEBUG =========="); + + // Print matched text + int a = ctx.start.getStartIndex(); + int b = ctx.stop.getStopIndex(); + Interval interval = new Interval(a, b); + String matchedText = ctx.start.getInputStream().getText(interval); + System.out.println("Matched text: " + matchedText); + + // Print stack trace + StackTraceElement[] cause = Thread.currentThread().getStackTrace(); + System.out.print("Stack trace: "); + for (int i = 0; i < cause.length; i++) { + System.out.print(cause[i].getMethodName()); + if (i != cause.length - 1) System.out.print(", "); + } + System.out.println("."); + + System.out.println("==============================="); + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/AstVisitor.java b/core/src/main/java/org/lflang/analyses/c/AstVisitor.java new file mode 100644 index 0000000000..d25c9d0364 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/AstVisitor.java @@ -0,0 +1,25 @@ +package org.lflang.analyses.c; + +import java.util.List; + +/** Modeled after ParseTreeVisitor.class */ +public interface AstVisitor { + + /** + * Visit an AST, and return a user-defined result of the operation. + * + * @param tree The {@link CAst.AstNode} to visit. + * @return The result of visiting the parse tree. + */ + T visit(CAst.AstNode tree); + + /** + * Visit an AST with a list of other AST nodes holding some information, and return a user-defined + * result of the operation. + * + * @param tree The {@link CAst.AstNode} to visit. + * @param nodeList A list of {@link CAst.AstNode} passed down the recursive call. + * @return The result of visiting the parse tree. + */ + T visit(CAst.AstNode tree, List nodeList); +} diff --git a/core/src/main/java/org/lflang/analyses/c/BuildAstParseTreeVisitor.java b/core/src/main/java/org/lflang/analyses/c/BuildAstParseTreeVisitor.java new file mode 100644 index 0000000000..e8923a2ce4 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/BuildAstParseTreeVisitor.java @@ -0,0 +1,756 @@ +package org.lflang.analyses.c; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import org.lflang.MessageReporter; +import org.lflang.dsl.CBaseVisitor; +import org.lflang.dsl.CParser.*; + +/** This visitor class builds an AST from the parse tree of a C program */ +public class BuildAstParseTreeVisitor extends CBaseVisitor { + + /** Message reporter for reporting warnings and errors */ + MessageReporter messageReporter; + + /** Constructor */ + public BuildAstParseTreeVisitor(MessageReporter messageReporter) { + super(); + this.messageReporter = messageReporter; + } + + @Override + public CAst.AstNode visitBlockItemList(BlockItemListContext ctx) { + CAst.StatementSequenceNode stmtSeq = new CAst.StatementSequenceNode(); + // Populate the children. + for (BlockItemContext blockItem : ctx.blockItem()) { + stmtSeq.children.add(visit(blockItem)); + } + return stmtSeq; + } + + @Override + public CAst.AstNode visitBlockItem(BlockItemContext ctx) { + if (ctx.statement() != null) return visit(ctx.statement()); + else return visit(ctx.declaration()); + } + + @Override + public CAst.AstNode visitDeclaration(DeclarationContext ctx) { + if (ctx.declarationSpecifiers() != null && ctx.initDeclaratorList() != null) { + //// Extract type from declarationSpecifiers. + List declSpecList = + ctx.declarationSpecifiers().declarationSpecifier(); + + // Cannot handle more than 1 specifiers, e.g. static const int. + // We can augment the analytical capability later. + if (declSpecList.size() > 1) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "the analyzer cannot handle more than 1 specifiers,", + "e.g. static const int.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + // Check if the declaration specifier is a type specifier: e.g. int or long. + DeclarationSpecifierContext declSpec = declSpecList.get(0); + if (declSpec.typeSpecifier() == null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "only type specifiers are supported.", + "e.g. \"static const int\" is not analyzable.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + // Check if the type specifier is what we currently support. + // Right now we only support int, long, & double. + CAst.VariableNode.Type type; + ArrayList supportedTypes = + new ArrayList(Arrays.asList("int", "long", "double", "_Bool")); + if (declSpec.typeSpecifier().Int() != null + || declSpec.typeSpecifier().Long() != null + || declSpec.typeSpecifier().Double() != null) type = CAst.VariableNode.Type.INT; + else if (declSpec.typeSpecifier().Bool() != null) type = CAst.VariableNode.Type.BOOLEAN; + // Mark the declaration unanalyzable if the type is unsupported. + else { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "unsupported type detected at " + declSpec.typeSpecifier(), + "Only " + supportedTypes + " are supported.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + //// Extract variable name and value from initDeclaratorList. + List initDeclList = ctx.initDeclaratorList().initDeclarator(); + + // Cannot handle more than 1 initDeclarator: e.g. x = 1, y = 2; + // We can augment the analytical capability later. + if (initDeclList.size() > 1) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "more than 1 declarators are detected on a single line,", + "e.g. \"int x = 1, y = 2;\" is not yet analyzable.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + // Get the variable name from the declarator. + DeclaratorContext decl = initDeclList.get(0).declarator(); + if (decl.pointer() != null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "pointers are currently not supported,", + "e.g. \"int *x;\" is not yet analyzable.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + if (decl.gccDeclaratorExtension().size() > 0) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "GCC declarator extensions are currently not supported,", + "e.g. \"__asm\" and \"__attribute__\" are not yet analyzable.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + DirectDeclaratorContext directDecl = decl.directDeclarator(); + if (directDecl.Identifier() == null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "the variable identifier is missing.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + // Extract the name of the variable. + String name = directDecl.Identifier().getText(); + // Create a variable Ast node. + CAst.VariableNode variable = new CAst.VariableNode(type, name); + + //// Convert the initializer to a value. + + // Make sure that there is an initializer. + InitDeclaratorContext initDecl = initDeclList.get(0); + if (initDecl.initializer() == null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "the initializer is missing,", + "e.g. \"int x;\" is not yet analyzable.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + + // FIXME: Use UninitCAst.VariableNode to perform special encoding. + // return new UninitCAst.VariableNode(type, name); + } + + // Extract the primaryExpression from the initializer. + if (initDecl.initializer().assignmentExpression() == null + || initDecl.initializer().assignmentExpression().conditionalExpression() == null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "assignmentExpression or conditionalExpression is missing.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + // Finally return the assignment node. + CAst.AssignmentNode assignmentNode = new CAst.AssignmentNode(); + CAst.AstNode initNode = + visitAssignmentExpression(initDecl.initializer().assignmentExpression()); + assignmentNode.left = variable; + assignmentNode.right = initNode; + return assignmentNode; + } + // Return OpaqueNode as default. + return new CAst.OpaqueNode(); + } + + /** + * This visit function builds StatementSequenceNode, AssignmentNode, OpaqueNode, IfBlockNode, + * AdditionNode, SubtractionNode, MultiplicationNode, DivisionNode, EqualNode, NotEqualNode, + * LessThanNode, GreaterThanNode, LessEqualNode, GreaterEqualNode, SetPortNode, + * ScheduleActionNode. + * + * @param ctx + * @return + */ + @Override + public CAst.AstNode visitStatement(StatementContext ctx) { + if (ctx.compoundStatement() != null) { + BlockItemListContext bilCtx = ctx.compoundStatement().blockItemList(); + if (bilCtx != null) { + return visitBlockItemList(bilCtx); + } + } else if (ctx.expressionStatement() != null) { + ExpressionContext exprCtx = ctx.expressionStatement().expression(); + if (exprCtx != null) { + return visitExpression(exprCtx); + } + } else if (ctx.selectionStatement() != null) { + return visitSelectionStatement(ctx.selectionStatement()); + } + return new CAst.OpaqueNode(); + } + + @Override + public CAst.AstNode visitExpression(ExpressionContext ctx) { + if (ctx.assignmentExpression().size() == 1) { + return visitAssignmentExpression(ctx.assignmentExpression().get(0)); + } + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "only one assignmentExpression in an expression is currently supported.", + "Marking the statement as opaque.")); + return new CAst.OpaqueNode(); + } + + @Override + public CAst.AstNode visitPrimaryExpression(PrimaryExpressionContext ctx) { + if (ctx.Identifier() != null) { + return new CAst.VariableNode(ctx.Identifier().getText()); + } else if (ctx.Constant() != null) { + return new CAst.LiteralNode(ctx.Constant().getText()); + } else if (ctx.expression() != null) { + return visitExpression(ctx.expression()); + } + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "only identifier, constant, and expressions are supported in a primary expression.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + // FIXME: More checks needed. This implementation currently silently omit + // certain cases, such as arr[1]. + @Override + public CAst.AstNode visitPostfixExpression(PostfixExpressionContext ctx) { + if (ctx.PlusPlus().size() > 0 + || ctx.MinusMinus().size() > 0 + || ctx.Dot().size() > 0 + || (ctx.LeftBracket().size() > 0 && ctx.RightBracket().size() > 0)) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Postfix '++', '--', '.', '[]' are currently not supported.", + "Marking the statement as opaque.")); + return new CAst.OpaqueNode(); + } + // State variables on the self struct, ports and actions. + if (ctx.primaryExpression() != null + && ctx.Identifier().size() == 1 + && ctx.Arrow().size() == 1) { + CAst.AstNode primaryExprNode = visitPrimaryExpression(ctx.primaryExpression()); + if (primaryExprNode instanceof CAst.LiteralNode) { + throw new AssertionError("unreachable"); + } + CAst.VariableNode varNode = (CAst.VariableNode) primaryExprNode; + if (varNode.name.equals("self")) { + return new CAst.StateVarNode(ctx.Identifier().get(0).getText()); + } else if (ctx.Identifier().get(0).getText().equals("value")) { + return new CAst.TriggerValueNode(varNode.name); + } else if (ctx.Identifier().get(0).getText().equals("is_present")) { + return new CAst.TriggerIsPresentNode(varNode.name); + } else { + // Generic pointer dereference, unanalyzable. + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Generic pointer dereference is not supported in a postfix expression.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + } + // LF built-in function calls (set or schedule) + if (ctx.primaryExpression() != null + && ctx.argumentExpressionList().size() == 1 + && ctx.LeftParen() != null + && ctx.RightParen() != null) { + CAst.AstNode primaryExprNode = visitPrimaryExpression(ctx.primaryExpression()); + List params = + ctx.argumentExpressionList().get(0).assignmentExpression(); + if (primaryExprNode instanceof CAst.LiteralNode) { + throw new AssertionError("unreachable"); + } + CAst.VariableNode varNode = (CAst.VariableNode) primaryExprNode; + if (varNode.name.equals("lf_set")) { + // return a set port node. + if (params.size() != 2) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "lf_set must have 2 arguments. Detected " + + ctx.argumentExpressionList().size(), + "Marking the function call as opaque.")); + return new CAst.OpaqueNode(); + } + CAst.SetPortNode node = new CAst.SetPortNode(); + node.left = visitAssignmentExpression(params.get(0)); + node.right = visitAssignmentExpression(params.get(1)); + return node; + } else if (varNode.name.equals("lf_schedule")) { + // return a set port node. + if (params.size() != 2) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "lf_schedule must have two arguments. Detected " + + ctx.argumentExpressionList().size(), + "Marking the function call as opaque.")); + return new CAst.OpaqueNode(); + } + CAst.ScheduleActionNode node = new CAst.ScheduleActionNode(); + for (AssignmentExpressionContext param : params) { + node.children.add(visitAssignmentExpression(param)); + } + return node; + } else if (varNode.name.equals("lf_schedule_int")) { + // return a set port node. + if (params.size() != 3) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "lf_schedule_int must have three arguments. Detected " + + ctx.argumentExpressionList().size(), + "Marking the function call as opaque.")); + return new CAst.OpaqueNode(); + } + CAst.ScheduleActionIntNode node = new CAst.ScheduleActionIntNode(); + for (AssignmentExpressionContext param : params) { + node.children.add(visitAssignmentExpression(param)); + } + return node; + } else { + // Generic pointer dereference, unanalyzable. + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Generic pointer dereference and function calls are not supported in a postfix" + + " expression.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + } + // Variable or literal + if (ctx.primaryExpression() != null) { + return visitPrimaryExpression(ctx.primaryExpression()); + } + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "only an identifier, constant, state variable, port, and action are supported in a" + + " primary expression.", + "Marking the declaration as opaque.")); + return new CAst.OpaqueNode(); + } + + @Override + public CAst.AstNode visitUnaryExpression(UnaryExpressionContext ctx) { + // Check for prefixes and mark them as opaque (unsupported for now). + if (ctx.PlusPlus().size() > 0 || ctx.MinusMinus().size() > 0 || ctx.Sizeof().size() > 0) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Prefix '++', '--', and 'sizeof' are currently not supported.", + "Marking the statement as opaque.")); + AstUtils.printStackTraceAndMatchedText(ctx); + return new CAst.OpaqueNode(); + } + // Handle the postfixExpression rule + // (look up the grammar in C.g4 to get more details). + if (ctx.postfixExpression() != null) { + return visitPostfixExpression(ctx.postfixExpression()); + } + // Handle the unary operators '!' (logical not) + // and '-' (negative). + if (ctx.unaryOperator() != null && ctx.castExpression() != null) { + CAst.AstNodeUnary node; + if (ctx.unaryOperator().Not() != null) { + // Handle the logical not expression. + node = new CAst.LogicalNotNode(); + node.child = visitCastExpression(ctx.castExpression()); + return node; + } else if (ctx.unaryOperator().Minus() != null) { + // Handle negative numbers. + // -5 will be translated as -1 * (5) + // which is a NegativeNode with a + // LiteralNode inside. + // + // FIXME: Need to perform precise error handling + // because we will go from a castExpression to + // a Constant under primaryExpression and anything + // else matching besides Constant could be problematic. + // For example, we cannot have a NegativeNode with + // a StringLiteralNode inside. This can be caught by + // the GCC, but if compilation is not involved, it + // would be useful to catch it here ourselves. + node = new CAst.NegativeNode(); + node.child = visitCastExpression(ctx.castExpression()); + return node; + } + } + + // Mark all the remaining cases as opaque. + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "only postfixExpression and '!' in a unaryExpression is currently supported.", + "Marking the statement as opaque.")); + AstUtils.printStackTraceAndMatchedText(ctx); + return new CAst.OpaqueNode(); + } + + @Override + public CAst.AstNode visitCastExpression(CastExpressionContext ctx) { + if (ctx.unaryExpression() != null) { + return visitUnaryExpression(ctx.unaryExpression()); + } + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "only unaryExpression in a castExpression is currently supported.", + "Marking the statement as opaque.")); + return new CAst.OpaqueNode(); + } + + @Override + public CAst.AstNode visitMultiplicativeExpression(MultiplicativeExpressionContext ctx) { + if (ctx.castExpression().size() > 1) { + CAst.AstNodeBinary node; + if (ctx.Star().size() > 0) { + node = new CAst.MultiplicationNode(); + } else if (ctx.Div().size() > 0) { + node = new CAst.DivisionNode(); + } else if (ctx.Mod().size() > 0) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Mod expression '%' is currently unsupported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } else { + node = new CAst.AstNodeBinary(); + } + node.left = visitCastExpression(ctx.castExpression().get(0)); + node.right = visitCastExpression(ctx.castExpression().get(1)); + return node; + } + return visitCastExpression(ctx.castExpression().get(0)); + } + + @Override + public CAst.AstNode visitAdditiveExpression(AdditiveExpressionContext ctx) { + if (ctx.multiplicativeExpression().size() > 1) { + CAst.AstNodeBinary node; + if (ctx.Plus().size() > 0) { + node = new CAst.AdditionNode(); + } else if (ctx.Minus().size() > 0) { + node = new CAst.SubtractionNode(); + } else { + node = new CAst.AstNodeBinary(); + } + node.left = visitMultiplicativeExpression(ctx.multiplicativeExpression().get(0)); + node.right = visitMultiplicativeExpression(ctx.multiplicativeExpression().get(1)); + return node; + } + return visitMultiplicativeExpression(ctx.multiplicativeExpression().get(0)); + } + + @Override + public CAst.AstNode visitShiftExpression(ShiftExpressionContext ctx) { + if (ctx.additiveExpression().size() > 1) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Shift expression '<<' or '>>' is currently unsupported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + return visitAdditiveExpression(ctx.additiveExpression().get(0)); + } + + @Override + public CAst.AstNode visitRelationalExpression(RelationalExpressionContext ctx) { + if (ctx.shiftExpression().size() > 1) { + CAst.AstNodeBinary node; + if (ctx.Less().size() > 0) { + node = new CAst.LessThanNode(); + } else if (ctx.LessEqual().size() > 0) { + node = new CAst.LessEqualNode(); + } else if (ctx.Greater().size() > 0) { + node = new CAst.GreaterThanNode(); + } else if (ctx.GreaterEqual().size() > 0) { + node = new CAst.GreaterEqualNode(); + } else { + node = new CAst.AstNodeBinary(); + } + node.left = visitShiftExpression(ctx.shiftExpression().get(0)); + node.right = visitShiftExpression(ctx.shiftExpression().get(1)); + return node; + } + return visitShiftExpression(ctx.shiftExpression().get(0)); + } + + @Override + public CAst.AstNode visitEqualityExpression(EqualityExpressionContext ctx) { + if (ctx.relationalExpression().size() > 1) { + CAst.AstNodeBinary node; + if (ctx.Equal().size() > 0) { + node = new CAst.EqualNode(); + } else if (ctx.NotEqual().size() > 0) { + node = new CAst.NotEqualNode(); + } else { + node = new CAst.AstNodeBinary(); + } + node.left = visitRelationalExpression(ctx.relationalExpression().get(0)); + node.right = visitRelationalExpression(ctx.relationalExpression().get(1)); + return node; + } + return visitRelationalExpression(ctx.relationalExpression().get(0)); + } + + @Override + public CAst.AstNode visitAndExpression(AndExpressionContext ctx) { + if (ctx.equalityExpression().size() > 1) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "And expression '&' is currently unsupported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + return visitEqualityExpression(ctx.equalityExpression().get(0)); + } + + @Override + public CAst.AstNode visitExclusiveOrExpression(ExclusiveOrExpressionContext ctx) { + if (ctx.andExpression().size() > 1) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Exclusive Or '^' is currently unsupported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + return visitAndExpression(ctx.andExpression().get(0)); + } + + @Override + public CAst.AstNode visitInclusiveOrExpression(InclusiveOrExpressionContext ctx) { + if (ctx.exclusiveOrExpression().size() > 1) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Inclusive Or '|' is currently unsupported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + return visitExclusiveOrExpression(ctx.exclusiveOrExpression().get(0)); + } + + @Override + public CAst.AstNode visitLogicalAndExpression(LogicalAndExpressionContext ctx) { + if (ctx.inclusiveOrExpression().size() > 1) { + CAst.LogicalAndNode node = new CAst.LogicalAndNode(); + node.left = visitInclusiveOrExpression(ctx.inclusiveOrExpression().get(0)); + node.right = visitInclusiveOrExpression(ctx.inclusiveOrExpression().get(1)); + return node; + } + return visitInclusiveOrExpression(ctx.inclusiveOrExpression().get(0)); + } + + @Override + public CAst.AstNode visitLogicalOrExpression(LogicalOrExpressionContext ctx) { + if (ctx.logicalAndExpression().size() > 1) { + CAst.LogicalOrNode node = new CAst.LogicalOrNode(); + node.left = visitLogicalAndExpression(ctx.logicalAndExpression().get(0)); + node.right = visitLogicalAndExpression(ctx.logicalAndExpression().get(1)); + return node; + } + return visitLogicalAndExpression(ctx.logicalAndExpression().get(0)); + } + + @Override + public CAst.AstNode visitConditionalExpression(ConditionalExpressionContext ctx) { + if (ctx.expression() != null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Currently do not support inline conditional expression.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + return visitLogicalOrExpression(ctx.logicalOrExpression()); + } + + @Override + public CAst.AstNode visitAssignmentExpression(AssignmentExpressionContext ctx) { + if (ctx.conditionalExpression() != null) { + return visitConditionalExpression(ctx.conditionalExpression()); + } + if (ctx.unaryExpression() != null && ctx.assignmentExpression() != null) { + CAst.AstNodeBinary assignmentNode = new CAst.AssignmentNode(); + assignmentNode.left = visitUnaryExpression(ctx.unaryExpression()); + if (ctx.assignmentOperator().getText().equals("=")) { + assignmentNode.right = visitAssignmentExpression(ctx.assignmentExpression()); + } else if (ctx.assignmentOperator().getText().equals("+=")) { + CAst.AdditionNode subnode = new CAst.AdditionNode(); + subnode.left = visitUnaryExpression(ctx.unaryExpression()); + subnode.right = visitAssignmentExpression(ctx.assignmentExpression()); + assignmentNode.right = subnode; + } else if (ctx.assignmentOperator().getText().equals("-=")) { + CAst.SubtractionNode subnode = new CAst.SubtractionNode(); + subnode.left = visitUnaryExpression(ctx.unaryExpression()); + subnode.right = visitAssignmentExpression(ctx.assignmentExpression()); + assignmentNode.right = subnode; + } else if (ctx.assignmentOperator().getText().equals("*=")) { + CAst.MultiplicationNode subnode = new CAst.MultiplicationNode(); + subnode.left = visitUnaryExpression(ctx.unaryExpression()); + subnode.right = visitAssignmentExpression(ctx.assignmentExpression()); + assignmentNode.right = subnode; + } else if (ctx.assignmentOperator().getText().equals("/=")) { + CAst.DivisionNode subnode = new CAst.DivisionNode(); + subnode.left = visitUnaryExpression(ctx.unaryExpression()); + subnode.right = visitAssignmentExpression(ctx.assignmentExpression()); + assignmentNode.right = subnode; + } else { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Only '=', '+=', '-=', '*=', '/=' assignment operators are supported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + return assignmentNode; + } + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "DigitSequence in an assignmentExpression is currently not supported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + + @Override + public CAst.AstNode visitSelectionStatement(SelectionStatementContext ctx) { + if (ctx.Switch() != null) { + messageReporter + .nowhere() + .warning( + String.join( + " ", + "Warning (line " + ctx.getStart().getLine() + "):", + "Switch case statement is currently not supported.", + "Marking the expression as opaque.")); + return new CAst.OpaqueNode(); + } + CAst.IfBlockNode ifBlockNode = new CAst.IfBlockNode(); + CAst.IfBodyNode ifBodyNode = new CAst.IfBodyNode(); + ifBlockNode.left = visitExpression(ctx.expression()); + ifBlockNode.right = ifBodyNode; + ifBodyNode.left = visitStatement(ctx.statement().get(0)); + if (ctx.statement().size() > 1) { + ifBodyNode.right = visitStatement(ctx.statement().get(1)); + } + return ifBlockNode; + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/CAst.java b/core/src/main/java/org/lflang/analyses/c/CAst.java new file mode 100644 index 0000000000..4bb391be00 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/CAst.java @@ -0,0 +1,456 @@ +package org.lflang.analyses.c; + +import java.util.ArrayList; +import java.util.List; + +public class CAst { + + public static class AstNode implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitAstNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitAstNode(this, nodeList); + } + } + + public static class AstNodeUnary extends AstNode implements Visitable { + public AstNode child; + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitAstNodeUnary(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitAstNodeUnary(this, nodeList); + } + } + + public static class AstNodeBinary extends AstNode implements Visitable { + public AstNode left; + public AstNode right; + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitAstNodeBinary(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitAstNodeBinary(this, nodeList); + } + } + + /** An AST node class that can have a list of child nodes with arbitrary length */ + public static class AstNodeDynamic extends AstNode implements Visitable { + public ArrayList children = new ArrayList<>(); + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitAstNodeDynamic(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitAstNodeDynamic(this, nodeList); + } + } + + public static class AssignmentNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitAssignmentNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitAssignmentNode(this, nodeList); + } + } + + /** AST node for an IF block. The left node is the condition. The right node is the IF body. */ + public static class IfBlockNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitIfBlockNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitIfBlockNode(this, nodeList); + } + } + + /** + * AST node for the body of an IF block. The left node is the THEN branch. The right node is the + * ELSE branch. + */ + public static class IfBodyNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitIfBodyNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitIfBodyNode(this, nodeList); + } + } + + public static class LiteralNode extends AstNode implements Visitable { + public String literal; + + public LiteralNode(String literal) { + super(); + this.literal = literal; + } + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitLiteralNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitLiteralNode(this, nodeList); + } + } + + public static class LogicalNotNode extends AstNodeUnary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitLogicalNotNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitLogicalNotNode(this, nodeList); + } + } + + public static class LogicalAndNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitLogicalAndNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitLogicalAndNode(this, nodeList); + } + } + + public static class LogicalOrNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitLogicalOrNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitLogicalOrNode(this, nodeList); + } + } + + /** An Ast node that indicates the code represented by this node is unanalyzable. */ + public static class OpaqueNode extends AstNode implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitOpaqueNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitOpaqueNode(this, nodeList); + } + } + + public static class StatementSequenceNode extends AstNodeDynamic implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitStatementSequenceNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitStatementSequenceNode(this, nodeList); + } + } + + public static class VariableNode extends AstNode implements Visitable { + public enum Type { + UNKNOWN, + INT, + BOOLEAN + } + + public Type type; + public String name; + + public VariableNode(String name) { + super(); + this.type = Type.UNKNOWN; + this.name = name; + } + + public VariableNode(Type type, String name) { + super(); + this.type = type; + this.name = name; + } + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitVariableNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitVariableNode(this, nodeList); + } + } + + /** Arithmetic operations */ + public static class AdditionNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitAdditionNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitAdditionNode(this, nodeList); + } + } + + public static class SubtractionNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitSubtractionNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitSubtractionNode(this, nodeList); + } + } + + public static class MultiplicationNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitMultiplicationNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitMultiplicationNode(this, nodeList); + } + } + + public static class DivisionNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitDivisionNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitDivisionNode(this, nodeList); + } + } + + /** Comparison operators */ + public static class EqualNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitEqualNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitEqualNode(this, nodeList); + } + } + + public static class NotEqualNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitNotEqualNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitNotEqualNode(this, nodeList); + } + } + + public static class NegativeNode extends AstNodeUnary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitNegativeNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitNegativeNode(this, nodeList); + } + } + + public static class LessThanNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitLessThanNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitLessThanNode(this, nodeList); + } + } + + public static class LessEqualNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitLessEqualNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitLessEqualNode(this, nodeList); + } + } + + public static class GreaterThanNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitGreaterThanNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitGreaterThanNode(this, nodeList); + } + } + + public static class GreaterEqualNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitGreaterEqualNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitGreaterEqualNode(this, nodeList); + } + } + + /** LF built-in operations */ + /** + * AST node for an lf_set call. The left child is the port being set. The right node is the value + * of the port. + */ + public static class SetPortNode extends AstNodeBinary implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitSetPortNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitSetPortNode(this, nodeList); + } + } + + /** AST node for a `lf_schedule(action, additional_delay)` call. */ + public static class ScheduleActionNode extends AstNodeDynamic implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitScheduleActionNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitScheduleActionNode(this, nodeList); + } + } + + /** AST node for a `lf_schedule_int(action, additional_delay, integer)` call. */ + public static class ScheduleActionIntNode extends AstNodeDynamic implements Visitable { + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitScheduleActionIntNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitScheduleActionIntNode(this, nodeList); + } + } + + /** + * Handle state variables appearing as self->. If the state variable appears on both sides + * of an assignment, such as `self-> = self-> + 1`, then `self->` on the RHS is + * marked as a "previous state" with `prev` set to true. + */ + public static class StateVarNode extends AstNode implements Visitable { + public String name; + public boolean prev = false; // By default, this is not a previous state. + + public StateVarNode(String name) { + this.name = name; + } + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitStateVarNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitStateVarNode(this, nodeList); + } + } + + /** Handle trigger values appearing as ->value */ + public static class TriggerValueNode extends AstNode implements Visitable { + public String name; + + public TriggerValueNode(String name) { + this.name = name; + } + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitTriggerValueNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitTriggerValueNode(this, nodeList); + } + } + + /** Handle trigger presence appearing as ->is_present */ + public static class TriggerIsPresentNode extends AstNode implements Visitable { + public String name; + + public TriggerIsPresentNode(String name) { + this.name = name; + } + + @Override + public T accept(AstVisitor visitor) { + return ((CAstVisitor) visitor).visitTriggerIsPresentNode(this); + } + + @Override + public T accept(AstVisitor visitor, List nodeList) { + return ((CAstVisitor) visitor).visitTriggerIsPresentNode(this, nodeList); + } + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/CAstVisitor.java b/core/src/main/java/org/lflang/analyses/c/CAstVisitor.java new file mode 100644 index 0000000000..d3c8f5c28d --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/CAstVisitor.java @@ -0,0 +1,132 @@ +package org.lflang.analyses.c; + +import java.util.List; + +/** Modeled after CVisitor.java */ +public interface CAstVisitor extends AstVisitor { + + T visitAstNode(CAst.AstNode node); + + T visitAstNodeUnary(CAst.AstNodeUnary node); + + T visitAstNodeBinary(CAst.AstNodeBinary node); + + T visitAstNodeDynamic(CAst.AstNodeDynamic node); + + T visitAssignmentNode(CAst.AssignmentNode node); + + T visitIfBlockNode(CAst.IfBlockNode node); + + T visitIfBodyNode(CAst.IfBodyNode node); + + T visitLiteralNode(CAst.LiteralNode node); + + T visitLogicalNotNode(CAst.LogicalNotNode node); + + T visitLogicalAndNode(CAst.LogicalAndNode node); + + T visitLogicalOrNode(CAst.LogicalOrNode node); + + T visitOpaqueNode(CAst.OpaqueNode node); + + T visitStatementSequenceNode(CAst.StatementSequenceNode node); + + T visitVariableNode(CAst.VariableNode node); + + T visitAdditionNode(CAst.AdditionNode node); + + T visitSubtractionNode(CAst.SubtractionNode node); + + T visitMultiplicationNode(CAst.MultiplicationNode node); + + T visitDivisionNode(CAst.DivisionNode node); + + T visitEqualNode(CAst.EqualNode node); + + T visitNotEqualNode(CAst.NotEqualNode node); + + T visitNegativeNode(CAst.NegativeNode node); + + T visitLessThanNode(CAst.LessThanNode node); + + T visitLessEqualNode(CAst.LessEqualNode node); + + T visitGreaterThanNode(CAst.GreaterThanNode node); + + T visitGreaterEqualNode(CAst.GreaterEqualNode node); + + T visitSetPortNode(CAst.SetPortNode node); + + T visitScheduleActionNode(CAst.ScheduleActionNode node); + + T visitScheduleActionIntNode(CAst.ScheduleActionIntNode node); + + T visitStateVarNode(CAst.StateVarNode node); + + T visitTriggerValueNode(CAst.TriggerValueNode node); + + T visitTriggerIsPresentNode(CAst.TriggerIsPresentNode node); + + /** Used for converting an AST into If Normal Form. */ + T visitAstNode(CAst.AstNode node, List nodeList); + + T visitAstNodeUnary(CAst.AstNodeUnary node, List nodeList); + + T visitAstNodeBinary(CAst.AstNodeBinary node, List nodeList); + + T visitAstNodeDynamic(CAst.AstNodeDynamic node, List nodeList); + + T visitAssignmentNode(CAst.AssignmentNode node, List nodeList); + + T visitIfBlockNode(CAst.IfBlockNode node, List nodeList); + + T visitIfBodyNode(CAst.IfBodyNode node, List nodeList); + + T visitLiteralNode(CAst.LiteralNode node, List nodeList); + + T visitLogicalNotNode(CAst.LogicalNotNode node, List nodeList); + + T visitLogicalAndNode(CAst.LogicalAndNode node, List nodeList); + + T visitLogicalOrNode(CAst.LogicalOrNode node, List nodeList); + + T visitOpaqueNode(CAst.OpaqueNode node, List nodeList); + + T visitStatementSequenceNode(CAst.StatementSequenceNode node, List nodeList); + + T visitVariableNode(CAst.VariableNode node, List nodeList); + + T visitAdditionNode(CAst.AdditionNode node, List nodeList); + + T visitSubtractionNode(CAst.SubtractionNode node, List nodeList); + + T visitMultiplicationNode(CAst.MultiplicationNode node, List nodeList); + + T visitDivisionNode(CAst.DivisionNode node, List nodeList); + + T visitEqualNode(CAst.EqualNode node, List nodeList); + + T visitNotEqualNode(CAst.NotEqualNode node, List nodeList); + + T visitNegativeNode(CAst.NegativeNode node, List nodeList); + + T visitLessThanNode(CAst.LessThanNode node, List nodeList); + + T visitLessEqualNode(CAst.LessEqualNode node, List nodeList); + + T visitGreaterThanNode(CAst.GreaterThanNode node, List nodeList); + + T visitGreaterEqualNode(CAst.GreaterEqualNode node, List nodeList); + + T visitSetPortNode(CAst.SetPortNode node, List nodeList); + + T visitScheduleActionNode(CAst.ScheduleActionNode node, List nodeList); + + T visitScheduleActionIntNode(CAst.ScheduleActionIntNode node, List nodeList); + + T visitStateVarNode(CAst.StateVarNode node, List nodeList); + + T visitTriggerValueNode(CAst.TriggerValueNode node, List nodeList); + + T visitTriggerIsPresentNode(CAst.TriggerIsPresentNode node, List nodeList); +} diff --git a/core/src/main/java/org/lflang/analyses/c/CBaseAstVisitor.java b/core/src/main/java/org/lflang/analyses/c/CBaseAstVisitor.java new file mode 100644 index 0000000000..11c2df3ef6 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/CBaseAstVisitor.java @@ -0,0 +1,352 @@ +package org.lflang.analyses.c; + +import java.util.List; + +/** + * A base class that provides default implementations of the visit functions. Other C AST visitors + * extend this class. + */ +public class CBaseAstVisitor extends AbstractAstVisitor implements CAstVisitor { + + /** + * These default implementations are not meant to be used. They should be overriden by the child + * class. In theory, this base visitor can be deleted? Let's keep it here for now for consistency. + */ + @Override + public T visitAstNode(CAst.AstNode node) { + return null; + } + + @Override + public T visitAstNodeUnary(CAst.AstNodeUnary node) { + if (node.child != null) { + T result = visit(node.child); + } else { + System.out.println("*** Child is empty in " + node + "!"); + } + return null; + } + + @Override + public T visitAstNodeBinary(CAst.AstNodeBinary node) { + if (node.left != null) { + T leftResult = visit(node.left); + } else { + System.out.println("*** Left child is empty in " + node + "!"); + } + if (node.right != null) { + T rightResult = visit(node.right); + } else { + System.out.println("*** Right child is empty in " + node + "!"); + } + // Aggregate results... + return null; + } + + @Override + public T visitAstNodeDynamic(CAst.AstNodeDynamic node) { + for (CAst.AstNode n : node.children) { + T result = visit(n); + } + return null; + } + + @Override + public T visitAssignmentNode(CAst.AssignmentNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitIfBlockNode(CAst.IfBlockNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitIfBodyNode(CAst.IfBodyNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitLiteralNode(CAst.LiteralNode node) { + return null; + } + + @Override + public T visitLogicalNotNode(CAst.LogicalNotNode node) { + return visitAstNodeUnary(node); + } + + @Override + public T visitLogicalAndNode(CAst.LogicalAndNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitLogicalOrNode(CAst.LogicalOrNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitOpaqueNode(CAst.OpaqueNode node) { + return visitAstNode(node); + } + + @Override + public T visitStatementSequenceNode(CAst.StatementSequenceNode node) { + return visitAstNodeDynamic(node); + } + + @Override + public T visitVariableNode(CAst.VariableNode node) { + return null; + } + + /** Arithmetic operators */ + @Override + public T visitAdditionNode(CAst.AdditionNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitSubtractionNode(CAst.SubtractionNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitMultiplicationNode(CAst.MultiplicationNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitDivisionNode(CAst.DivisionNode node) { + return visitAstNodeBinary(node); + } + + /** Comparison operators */ + @Override + public T visitEqualNode(CAst.EqualNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitNotEqualNode(CAst.NotEqualNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitNegativeNode(CAst.NegativeNode node) { + return visitNegativeNode(node); + } + + @Override + public T visitLessThanNode(CAst.LessThanNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitLessEqualNode(CAst.LessEqualNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitGreaterThanNode(CAst.GreaterThanNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitGreaterEqualNode(CAst.GreaterEqualNode node) { + return visitAstNodeBinary(node); + } + + /** LF built-in operations */ + @Override + public T visitSetPortNode(CAst.SetPortNode node) { + return visitAstNodeBinary(node); + } + + @Override + public T visitScheduleActionNode(CAst.ScheduleActionNode node) { + return visitAstNodeDynamic(node); + } + + @Override + public T visitScheduleActionIntNode(CAst.ScheduleActionIntNode node) { + return visitAstNodeDynamic(node); + } + + @Override + public T visitStateVarNode(CAst.StateVarNode node) { + return null; + } + + @Override + public T visitTriggerValueNode(CAst.TriggerValueNode node) { + return null; + } + + @Override + public T visitTriggerIsPresentNode(CAst.TriggerIsPresentNode node) { + return null; + } + + //// With one more parameter. + @Override + public T visitAstNode(CAst.AstNode node, List nodeList) { + return visitAstNode(node); + } + + @Override + public T visitAstNodeUnary(CAst.AstNodeUnary node, List nodeList) { + return visitAstNodeUnary(node); + } + + @Override + public T visitAstNodeBinary(CAst.AstNodeBinary node, List nodeList) { + return visitAstNodeBinary(node); + } + + @Override + public T visitAstNodeDynamic(CAst.AstNodeDynamic node, List nodeList) { + return visitAstNodeDynamic(node); + } + + @Override + public T visitAssignmentNode(CAst.AssignmentNode node, List nodeList) { + return visitAssignmentNode(node); + } + + @Override + public T visitIfBlockNode(CAst.IfBlockNode node, List nodeList) { + return visitIfBlockNode(node); + } + + @Override + public T visitIfBodyNode(CAst.IfBodyNode node, List nodeList) { + return visitIfBodyNode(node); + } + + @Override + public T visitLiteralNode(CAst.LiteralNode node, List nodeList) { + return visitLiteralNode(node); + } + + @Override + public T visitLogicalNotNode(CAst.LogicalNotNode node, List nodeList) { + return visitLogicalNotNode(node); + } + + @Override + public T visitLogicalAndNode(CAst.LogicalAndNode node, List nodeList) { + return visitLogicalAndNode(node); + } + + @Override + public T visitLogicalOrNode(CAst.LogicalOrNode node, List nodeList) { + return visitLogicalOrNode(node); + } + + @Override + public T visitOpaqueNode(CAst.OpaqueNode node, List nodeList) { + return visitOpaqueNode(node); + } + + @Override + public T visitStatementSequenceNode( + CAst.StatementSequenceNode node, List nodeList) { + return visitStatementSequenceNode(node); + } + + @Override + public T visitVariableNode(CAst.VariableNode node, List nodeList) { + return visitVariableNode(node); + } + + /** Arithmetic operators */ + @Override + public T visitAdditionNode(CAst.AdditionNode node, List nodeList) { + return visitAdditionNode(node); + } + + @Override + public T visitSubtractionNode(CAst.SubtractionNode node, List nodeList) { + return visitSubtractionNode(node); + } + + @Override + public T visitMultiplicationNode(CAst.MultiplicationNode node, List nodeList) { + return visitMultiplicationNode(node); + } + + @Override + public T visitDivisionNode(CAst.DivisionNode node, List nodeList) { + return visitDivisionNode(node); + } + + /** Comparison operators */ + @Override + public T visitEqualNode(CAst.EqualNode node, List nodeList) { + return visitEqualNode(node); + } + + @Override + public T visitNotEqualNode(CAst.NotEqualNode node, List nodeList) { + return visitNotEqualNode(node); + } + + @Override + public T visitNegativeNode(CAst.NegativeNode node, List nodeList) { + return visitNegativeNode(node); + } + + @Override + public T visitLessThanNode(CAst.LessThanNode node, List nodeList) { + return visitLessThanNode(node); + } + + @Override + public T visitLessEqualNode(CAst.LessEqualNode node, List nodeList) { + return visitLessEqualNode(node); + } + + @Override + public T visitGreaterThanNode(CAst.GreaterThanNode node, List nodeList) { + return visitGreaterThanNode(node); + } + + @Override + public T visitGreaterEqualNode(CAst.GreaterEqualNode node, List nodeList) { + return visitGreaterEqualNode(node); + } + + /** LF built-in operations */ + @Override + public T visitSetPortNode(CAst.SetPortNode node, List nodeList) { + return visitSetPortNode(node); + } + + @Override + public T visitScheduleActionNode(CAst.ScheduleActionNode node, List nodeList) { + return visitScheduleActionNode(node); + } + + @Override + public T visitScheduleActionIntNode( + CAst.ScheduleActionIntNode node, List nodeList) { + return visitScheduleActionIntNode(node); + } + + @Override + public T visitStateVarNode(CAst.StateVarNode node, List nodeList) { + return visitStateVarNode(node); + } + + @Override + public T visitTriggerValueNode(CAst.TriggerValueNode node, List nodeList) { + return visitTriggerValueNode(node); + } + + @Override + public T visitTriggerIsPresentNode(CAst.TriggerIsPresentNode node, List nodeList) { + return visitTriggerIsPresentNode(node); + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/CToUclidVisitor.java b/core/src/main/java/org/lflang/analyses/c/CToUclidVisitor.java new file mode 100644 index 0000000000..0608387abb --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/CToUclidVisitor.java @@ -0,0 +1,420 @@ +package org.lflang.analyses.c; + +import java.util.ArrayList; +import java.util.List; +import org.lflang.analyses.c.CAst.*; +import org.lflang.analyses.uclid.UclidGenerator; +import org.lflang.generator.ActionInstance; +import org.lflang.generator.NamedInstance; +import org.lflang.generator.PortInstance; +import org.lflang.generator.ReactionInstance; +import org.lflang.generator.ReactorInstance; +import org.lflang.generator.StateVariableInstance; +import org.lflang.generator.TriggerInstance; + +public class CToUclidVisitor extends CBaseAstVisitor { + + /** The Uclid generator instance */ + private UclidGenerator generator; + + /** The reaction instance for the generated axiom */ + private ReactionInstance.Runtime reaction; + + /** The reactor that contains the reaction */ + private ReactorInstance reactor; + + /** A list of all the named instances */ + private List instances = new ArrayList(); + + /** Quantified variable */ + private final String qv = "i"; + + private final String qv2 = "j"; + + /** Unchanged variables and triggers */ + private List unchangedStates; + + private List unchangedTriggers; + + // FIXME: Make this more flexible and infer value from program. + /** Default reset value */ + private final String defaultValue = "0"; + + private final String defaultPresence = "false"; + + /** Constructor */ + public CToUclidVisitor(UclidGenerator generator, ReactionInstance.Runtime reaction) { + this.generator = generator; + this.reaction = reaction; + this.reactor = reaction.getReaction().getParent(); + instances.addAll(this.reactor.inputs); + instances.addAll(this.reactor.outputs); + instances.addAll(this.reactor.actions); + instances.addAll(this.reactor.states); + } + + @Override + public String visitAdditionNode(AdditionNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " + " + rhs + ")"; + } + + @Override + public String visitAssignmentNode(AssignmentNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " == " + rhs + ")"; + } + + @Override + public String visitDivisionNode(DivisionNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " / " + rhs + ")"; + } + + @Override + public String visitEqualNode(EqualNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " == " + rhs + ")"; + } + + @Override + public String visitGreaterEqualNode(GreaterEqualNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " >= " + rhs + ")"; + } + + @Override + public String visitGreaterThanNode(GreaterThanNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " > " + rhs + ")"; + } + + @Override + public String visitIfBlockNode(IfBlockNode node) { + String antecedent = visit(node.left); // Process if condition + String consequent = visit(((IfBodyNode) node.right).left); + return "(" + antecedent + " ==> " + "(" + consequent + "\n))"; + } + + @Override + public String visitLessEqualNode(LessEqualNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " <= " + rhs + ")"; + } + + @Override + public String visitLessThanNode(LessThanNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " < " + rhs + ")"; + } + + @Override + public String visitLiteralNode(LiteralNode node) { + return node.literal; + } + + @Override + public String visitLogicalAndNode(LogicalAndNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " && " + rhs + ")"; + } + + @Override + public String visitLogicalNotNode(LogicalNotNode node) { + return "!" + "(" + visit(node.child) + ")"; + } + + @Override + public String visitLogicalOrNode(LogicalOrNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " || " + rhs + ")"; + } + + @Override + public String visitMultiplicationNode(MultiplicationNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " * " + rhs + ")"; + } + + @Override + public String visitNotEqualNode(NotEqualNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " != " + rhs + ")"; + } + + @Override + public String visitNegativeNode(NegativeNode node) { + return "(" + "-1*(" + visit(node.child) + "))"; + } + + @Override + public String visitScheduleActionNode(ScheduleActionNode node) { + String name = ((VariableNode) node.children.get(0)).name; + NamedInstance instance = getInstanceByName(name); + ActionInstance action = (ActionInstance) instance; + String additionalDelay = visit(node.children.get(1)); + String str = + "\n(" + + "(finite_exists (" + + this.qv2 + + " : integer) in indices :: (" + + this.qv2 + + " > " + + this.qv + + " && " + + this.qv2 + + " <= END_TRACE) && (" + + "\n " + + action.getFullNameWithJoiner("_") + + "_is_present" + + "(" + + "t" + + "(" + + this.qv2 + + ")" + + ")" + + "\n " + + "&& " + + "tag_same" + + "(" + + "g(" + + this.qv2 + + ")" + + ", " + + "tag_schedule" + + "(" + + "g" + + "(" + + this.qv + + ")" + + ", " + + "(" + + action.getMinDelay().toNanoSeconds() + + "+" + + additionalDelay + + ")" + + ")" + + ")" + + "\n " + + "&& " + + action.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + this.qv2 + + ")" + + ")" + + " == " + + "0" + + "\n)) // Closes finite_exists" + + "\n&& " + + action.getFullNameWithJoiner("_") + + "_scheduled" + + "(" + + "d" + + "(" + + this.qv + + ")" + + ")" + + "\n)"; + return str; + } + + @Override + public String visitScheduleActionIntNode(ScheduleActionIntNode node) { + String name = ((VariableNode) node.children.get(0)).name; + NamedInstance instance = getInstanceByName(name); + ActionInstance action = (ActionInstance) instance; + String additionalDelay = visit(node.children.get(1)); + String intValue = visit(node.children.get(2)); + String str = + "\n(" + + "(finite_exists (" + + this.qv2 + + " : integer) in indices :: (" + + this.qv2 + + " > " + + this.qv + + " && " + + this.qv2 + + " <= END_TRACE) && (" + + "\n " + + action.getFullNameWithJoiner("_") + + "_is_present" + + "(" + + "t" + + "(" + + this.qv2 + + ")" + + ")" + + "\n " + + "&& " + + "tag_same" + + "(" + + "g(" + + this.qv2 + + ")" + + ", " + + "tag_schedule" + + "(" + + "g" + + "(" + + this.qv + + ")" + + ", " + + "(" + + action.getMinDelay().toNanoSeconds() + + "+" + + additionalDelay + + ")" + + ")" + + ")" + + "\n)) // Closes finite_exists" + + "\n&& " + + action.getFullNameWithJoiner("_") + + "_scheduled" + + "(" + + "d" + + "(" + + this.qv + + ")" + + ")" + + "\n&& " + + action.getFullNameWithJoiner("_") + + "_scheduled_payload" + + "(" + + "pl" + + "(" + + this.qv + + ")" + + ")" + + " == " + + intValue + + "\n)"; + return str; + } + + @Override + public String visitSetPortNode(SetPortNode node) { + NamedInstance port = getInstanceByName(((VariableNode) node.left).name); + String value = visit(node.right); + // Remove this port from the unchanged list. + // this.unchangedTriggers.remove(port); + return "(" + + "(" + + port.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + this.qv + + ")" + + ")" + + " == " + + value + + ")" + + " && " + + "(" + + port.getFullNameWithJoiner("_") + + "_is_present" + + "(" + + "t" + + "(" + + this.qv + + ")" + + ")" + + ")" + + ")"; + } + + @Override + public String visitStateVarNode(StateVarNode node) { + NamedInstance instance = getInstanceByName(node.name); + return instance.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + this.qv + + (node.prev ? "-1" : "") + + ")" + + ")"; + } + + @Override + public String visitStatementSequenceNode(StatementSequenceNode node) { + String axiom = ""; + for (int i = 0; i < node.children.size(); i++) { + axiom += visit(node.children.get(i)); + if (i != node.children.size() - 1) axiom += "\n" + " " + "&& "; + } + return axiom; + } + + @Override + public String visitSubtractionNode(SubtractionNode node) { + String lhs = visit(node.left); + String rhs = visit(node.right); + return "(" + lhs + " - " + rhs + ")"; + } + + @Override + public String visitTriggerIsPresentNode(TriggerIsPresentNode node) { + // Find the trigger instance by name. + NamedInstance instance = getInstanceByName(node.name); + return instance.getFullNameWithJoiner("_") + + "_is_present" + + "(" + + "t" + + "(" + + this.qv + + ")" + + ")"; + } + + @Override + public String visitTriggerValueNode(TriggerValueNode node) { + // Find the trigger instance by name. + NamedInstance instance = getInstanceByName(node.name); + return instance.getFullNameWithJoiner("_") + "(" + "s" + "(" + this.qv + ")" + ")"; + } + + @Override + public String visitVariableNode(VariableNode node) { + NamedInstance instance = getInstanceByName(node.name); + return instance.getFullNameWithJoiner("_") + "(" + "s" + "(" + this.qv + ")" + ")"; + } + + ///////////////////////////// + //// Private functions + + /** Look up an instance by name. This function throws an error if an instance is not found. */ + private NamedInstance getInstanceByName(String name) { + for (NamedInstance i : this.instances) { + if (i instanceof ActionInstance) { + if (((ActionInstance) i).getDefinition().getName().equals(name)) { + return i; + } + } else if (i instanceof PortInstance) { + if (((PortInstance) i).getDefinition().getName().equals(name)) { + return i; + } + } else if (i instanceof StateVariableInstance) { + if (((StateVariableInstance) i).getDefinition().getName().equals(name)) { + return i; + } + } + } + throw new RuntimeException("NamedInstance not found!"); + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/IfNormalFormAstVisitor.java b/core/src/main/java/org/lflang/analyses/c/IfNormalFormAstVisitor.java new file mode 100644 index 0000000000..d51bec6aad --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/IfNormalFormAstVisitor.java @@ -0,0 +1,91 @@ +package org.lflang.analyses.c; + +import java.util.ArrayList; +import java.util.List; + +/** + * An AST visitor that converts an original AST into the If Normal Form. See "Bounded Model Checking + * of Software using SMT Solvers instead of SAT Solvers" for details about the If Normal Form + * (https://link.springer.com/chapter/10.1007/11691617_9). + * + *

There are several requirements for an AST to be in INF: 1. There should be a single + * StatementSequence (SS) root node; 2. Each child of the SS node should be an IfBlockNode; 3. + * Variables in a subsequent child should be marked as "primed" versions of those in the previous + * child. + * + *

Limitations: 1. The implementation does not take the scope into account. E.g. "int i = 0; { + * int j = 0; }" is treated the same as "int i = 0; int j = 0;". 2. Due to the above limitation, the + * implementation assumes that each variable has a unique name. E.g. "{ int i = 0; }{ int i = 0; }" + * is an ill-formed program. + * + *

In this program, visit() is the normalise() in the paper. + */ +public class IfNormalFormAstVisitor extends CBaseAstVisitor { + + public CAst.StatementSequenceNode INF = new CAst.StatementSequenceNode(); + + @Override + public Void visitStatementSequenceNode( + CAst.StatementSequenceNode node, List conditions) { + for (CAst.AstNode child : node.children) { + visit(child, conditions); + } + return null; + } + + @Override + public Void visitAssignmentNode(CAst.AssignmentNode node, List conditions) { + this.INF.children.add(generateIfBlock(node, conditions)); + return null; + } + + @Override + public Void visitSetPortNode(CAst.SetPortNode node, List conditions) { + this.INF.children.add(generateIfBlock(node, conditions)); + return null; + } + + @Override + public Void visitScheduleActionNode(CAst.ScheduleActionNode node, List conditions) { + this.INF.children.add(generateIfBlock(node, conditions)); + return null; + } + + @Override + public Void visitScheduleActionIntNode( + CAst.ScheduleActionIntNode node, List conditions) { + this.INF.children.add(generateIfBlock(node, conditions)); + return null; + } + + @Override + public Void visitIfBlockNode(CAst.IfBlockNode node, List conditions) { + List leftConditions = new ArrayList<>(conditions); + leftConditions.add(node.left); + visit(((CAst.IfBodyNode) node.right).left, leftConditions); + if (((CAst.IfBodyNode) node.right).right != null) { + List rightConditions = new ArrayList<>(conditions); + // Add a not node. + CAst.LogicalNotNode notNode = new CAst.LogicalNotNode(); + notNode.child = node.left; // Negate the condition. + rightConditions.add(notNode); + visit(((CAst.IfBodyNode) node.right).right, rightConditions); + } + return null; + } + + private CAst.IfBlockNode generateIfBlock(CAst.AstNode node, List conditions) { + // Create an If Block node. + CAst.IfBlockNode ifNode = new CAst.IfBlockNode(); + // Set the condition of the if block node. + CAst.AstNode conjunction = AstUtils.takeConjunction(conditions); + ifNode.left = conjunction; + // Create a new body node. + CAst.IfBodyNode body = new CAst.IfBodyNode(); + ifNode.right = body; + // Set the then branch to the assignment. + body.left = node; + + return ifNode; + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/VariablePrecedenceVisitor.java b/core/src/main/java/org/lflang/analyses/c/VariablePrecedenceVisitor.java new file mode 100644 index 0000000000..9354e36269 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/VariablePrecedenceVisitor.java @@ -0,0 +1,42 @@ +package org.lflang.analyses.c; + +import org.lflang.analyses.c.CAst.*; + +/** This visitor marks certain variable node as "previous." */ +public class VariablePrecedenceVisitor extends CBaseAstVisitor { + + // This is a temporary solution and cannot handle, + // e.g., self->s = (self->s + 1) - (2 * 2). + @Override + public Void visitAssignmentNode(AssignmentNode node) { + if (node.left instanceof StateVarNode) { + if (node.right instanceof AstNodeBinary) { + AstNodeBinary n = (AstNodeBinary) node.right; + if (n.left instanceof StateVarNode) { + ((StateVarNode) n.left).prev = true; + } + if (n.right instanceof StateVarNode) { + ((StateVarNode) n.right).prev = true; + } + } + } else { + throw new AssertionError("unreachable"); + } + return null; + } + + @Override + public Void visitIfBlockNode(IfBlockNode node) { + if (((IfBodyNode) node.right).left != null) visit(((IfBodyNode) node.right).left); + if (((IfBodyNode) node.right).right != null) visit(((IfBodyNode) node.right).right); + return null; + } + + @Override + public Void visitStatementSequenceNode(StatementSequenceNode node) { + for (int i = 0; i < node.children.size(); i++) { + visit(node.children.get(i)); + } + return null; + } +} diff --git a/core/src/main/java/org/lflang/analyses/c/Visitable.java b/core/src/main/java/org/lflang/analyses/c/Visitable.java new file mode 100644 index 0000000000..cbdea446ca --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/c/Visitable.java @@ -0,0 +1,12 @@ +package org.lflang.analyses.c; + +import java.util.List; + +public interface Visitable { + + /** The {@link AstVisitor} needs a double dispatch method. */ + T accept(AstVisitor visitor); + + /** The {@link AstVisitor} needs a double dispatch method. */ + T accept(AstVisitor visitor, List nodeList); +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/Event.java b/core/src/main/java/org/lflang/analyses/statespace/Event.java new file mode 100644 index 0000000000..d8613e5138 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/Event.java @@ -0,0 +1,51 @@ +package org.lflang.analyses.statespace; + +import org.lflang.generator.TriggerInstance; + +/** A node in the state space diagram representing a step in the execution of an LF program. */ +public class Event implements Comparable { + + private TriggerInstance trigger; + private Tag tag; + + public Event(TriggerInstance trigger, Tag tag) { + this.trigger = trigger; + this.tag = tag; + } + + /** + * Compare two events first by tags and, if tags are equal, by trigger names in lexical order. + * This is useful for enforcing a unique order of events in a priority queue of Event instances. + */ + @Override + public int compareTo(Event e) { + // Compare tags first. + int ret = this.tag.compareTo(e.getTag()); + // If tags match, compare trigger names. + if (ret == 0) ret = this.trigger.getFullName().compareTo(e.trigger.getFullName()); + return ret; + } + + /** This method checks if two events have the same triggers. */ + public boolean hasSameTriggers(Object o) { + if (o == null) return false; + if (o instanceof Event) { + Event e = (Event) o; + if (this.trigger.equals(e.trigger)) return true; + } + return false; + } + + @Override + public String toString() { + return "(" + trigger.getFullName() + ", " + tag + ")"; + } + + public Tag getTag() { + return tag; + } + + public TriggerInstance getTrigger() { + return trigger; + } +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/EventQueue.java b/core/src/main/java/org/lflang/analyses/statespace/EventQueue.java new file mode 100644 index 0000000000..7c04206da7 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/EventQueue.java @@ -0,0 +1,21 @@ +package org.lflang.analyses.statespace; + +import java.util.PriorityQueue; + +/** + * An event queue implementation that sorts events in the order of _time tags_ and _trigger names_ + * based on the implementation of compareTo() in the Event class. + */ +public class EventQueue extends PriorityQueue { + + /** + * Modify the original add() by enforcing uniqueness. There cannot be duplicate events in the + * event queue. + */ + @Override + public boolean add(Event e) { + if (this.contains(e)) return false; + super.add(e); + return true; + } +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/StateInfo.java b/core/src/main/java/org/lflang/analyses/statespace/StateInfo.java new file mode 100644 index 0000000000..89c3bd19de --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/StateInfo.java @@ -0,0 +1,24 @@ +package org.lflang.analyses.statespace; + +import java.util.ArrayList; +import java.util.HashMap; + +/** A class that represents information in a step in a counterexample trace */ +public class StateInfo { + + public ArrayList reactions = new ArrayList<>(); + public Tag tag; + public HashMap variables = new HashMap<>(); + public HashMap triggers = new HashMap<>(); + public HashMap scheduled = new HashMap<>(); + public HashMap payloads = new HashMap<>(); + + public void display() { + System.out.println("reactions: " + reactions); + System.out.println("tag: " + tag); + System.out.println("variables: " + variables); + System.out.println("triggers: " + triggers); + System.out.println("scheduled: " + scheduled); + System.out.println("payloads: " + payloads); + } +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/StateSpaceDiagram.java b/core/src/main/java/org/lflang/analyses/statespace/StateSpaceDiagram.java new file mode 100644 index 0000000000..e2aa66737d --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/StateSpaceDiagram.java @@ -0,0 +1,219 @@ +package org.lflang.analyses.statespace; + +import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; +import org.lflang.TimeValue; +import org.lflang.generator.CodeBuilder; +import org.lflang.generator.ReactionInstance; +import org.lflang.graph.DirectedGraph; + +/** A directed graph representing the state space of an LF program. */ +public class StateSpaceDiagram extends DirectedGraph { + + /** The first node of the state space diagram. */ + public StateSpaceNode head; + + /** The last node of the state space diagram. */ + public StateSpaceNode tail; + + /** + * The previously encountered node which the tail node goes back to, i.e. the location where the + * back loop happens. + */ + public StateSpaceNode loopNode; + + /** + * Store the state when the loop node is reached for the 2nd time. This is used to calculate the + * elapsed logical time on the back loop edge. + */ + public StateSpaceNode loopNodeNext; + + /** The logical time elapsed for each loop iteration. */ + public long loopPeriod; + + /** A dot file that represents the diagram */ + private CodeBuilder dot; + + /** */ + private final boolean compactDot = false; + + /** Before adding the node, assign it an index. */ + @Override + public void addNode(StateSpaceNode node) { + node.setIndex(this.nodeCount()); + super.addNode(node); + } + + /** Get the immediately downstream node. */ + public StateSpaceNode getDownstreamNode(StateSpaceNode node) { + Set downstream = this.getDownstreamAdjacentNodes(node); + if (downstream == null || downstream.size() == 0) return null; + return (StateSpaceNode) downstream.toArray()[0]; + } + + /** Pretty print the diagram. */ + public void display() { + System.out.println("*************************************************"); + System.out.println("* Pretty printing worst-case state space diagram:"); + long timestamp; + StateSpaceNode node = this.head; + if (node == null) { + System.out.println("* EMPTY"); + System.out.println("*************************************************"); + return; + } + while (node != this.tail) { + System.out.print("* State " + node.getIndex() + ": "); + node.display(); + + // Store the tag of the prior step. + timestamp = node.getTag().timestamp; + + // Assume a unique next state. + node = getDownstreamNode(node); + + // Compute time difference + if (node != null) { + TimeValue tsDiff = TimeValue.fromNanoSeconds(node.getTag().timestamp - timestamp); + System.out.println("* => Advance time by " + tsDiff); + } + } + + // Print tail node + System.out.print("* (Tail) state " + node.getIndex() + ": "); + node.display(); + + if (this.loopNode != null) { + // Compute time difference + TimeValue tsDiff = + TimeValue.fromNanoSeconds(loopNodeNext.getTag().timestamp - tail.getTag().timestamp); + System.out.println("* => Advance time by " + tsDiff); + + System.out.println("* Goes back to loop node: state " + this.loopNode.getIndex()); + System.out.print("* Loop node reached 2nd time: "); + this.loopNodeNext.display(); + } + System.out.println("*************************************************"); + } + + /** + * Generate a dot file from the state space diagram. + * + * @return a CodeBuilder with the generated code + */ + public CodeBuilder generateDot() { + if (dot == null) { + dot = new CodeBuilder(); + dot.pr("digraph G {"); + dot.indent(); + if (this.loopNode != null) { + dot.pr("layout=circo;"); + } + dot.pr("rankdir=LR;"); + if (this.compactDot) { + dot.pr("mindist=1.5;"); + dot.pr("overlap=false"); + dot.pr("node [shape=Mrecord fontsize=40]"); + dot.pr("edge [fontsize=40 penwidth=3 arrowsize=2]"); + } else { + dot.pr("node [shape=Mrecord]"); + } + // Generate a node for each state. + if (this.compactDot) { + for (StateSpaceNode n : this.nodes()) { + dot.pr( + "S" + + n.getIndex() + + " [" + + "label = \" {" + + "S" + + n.getIndex() + + " | " + + n.getReactionsInvoked().size() + + " | " + + n.getEventQcopy().size() + + "}" + + " | " + + n.getTag() + + "\"" + + "]"); + } + } else { + for (StateSpaceNode n : this.nodes()) { + List reactions = + n.getReactionsInvoked().stream() + .map(ReactionInstance::getFullName) + .collect(Collectors.toList()); + String reactionsStr = String.join("\\n", reactions); + List events = + n.getEventQcopy().stream().map(Event::toString).collect(Collectors.toList()); + String eventsStr = String.join("\\n", events); + dot.pr( + "S" + + n.getIndex() + + " [" + + "label = \"" + + "S" + + n.getIndex() + + " | " + + n.getTag() + + " | " + + "Reactions invoked:\\n" + + reactionsStr + + " | " + + "Pending events:\\n" + + eventsStr + + "\"" + + "]"); + } + } + + StateSpaceNode current = this.head; + StateSpaceNode next = getDownstreamNode(this.head); + while (current != null && next != null && current != this.tail) { + TimeValue tsDiff = + TimeValue.fromNanoSeconds(next.getTag().timestamp - current.getTag().timestamp); + dot.pr( + "S" + + current.getIndex() + + " -> " + + "S" + + next.getIndex() + + " [label = " + + "\"" + + "+" + + tsDiff + + "\"" + + "]"); + current = next; + next = getDownstreamNode(next); + } + + if (loopNode != null) { + TimeValue tsDiff = + TimeValue.fromNanoSeconds(loopNodeNext.getTag().timestamp - tail.getTag().timestamp); + TimeValue period = TimeValue.fromNanoSeconds(loopPeriod); + dot.pr( + "S" + + current.getIndex() + + " -> " + + "S" + + next.getIndex() + + " [label = " + + "\"" + + "+" + + tsDiff + + " -" + + period + + "\"" + + " weight = 0 " + + "]"); + } + + dot.unindent(); + dot.pr("}"); + } + return this.dot; + } +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/StateSpaceExplorer.java b/core/src/main/java/org/lflang/analyses/statespace/StateSpaceExplorer.java new file mode 100644 index 0000000000..48f407914f --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/StateSpaceExplorer.java @@ -0,0 +1,319 @@ +package org.lflang.analyses.statespace; + +import java.util.ArrayList; +import java.util.HashMap; +import java.util.HashSet; +import java.util.Set; +import org.lflang.TimeUnit; +import org.lflang.TimeValue; +import org.lflang.generator.ActionInstance; +import org.lflang.generator.PortInstance; +import org.lflang.generator.ReactionInstance; +import org.lflang.generator.ReactorInstance; +import org.lflang.generator.RuntimeRange; +import org.lflang.generator.SendRange; +import org.lflang.generator.TimerInstance; +import org.lflang.generator.TriggerInstance; +import org.lflang.lf.Expression; +import org.lflang.lf.Time; +import org.lflang.lf.Variable; + +/** + * (EXPERIMENTAL) Explores the state space of an LF program. Use with caution since this is + * experimental code. + */ +public class StateSpaceExplorer { + + // Instantiate an empty state space diagram. + public StateSpaceDiagram diagram = new StateSpaceDiagram(); + + // Indicate whether a back loop is found in the state space. + // A back loop suggests periodic behavior. + public boolean loopFound = false; + + /** + * Instantiate a global event queue. We will use this event queue to symbolically simulate the + * logical timeline. This simulation is also valid for runtime implementations that are federated + * or relax global barrier synchronization, since an LF program defines a unique logical timeline + * (assuming all reactions behave _consistently_ throughout the execution). + */ + public EventQueue eventQ = new EventQueue(); + + /** The main reactor instance based on which the state space is explored. */ + public ReactorInstance main; + + // Constructor + public StateSpaceExplorer(ReactorInstance main) { + this.main = main; + } + + /** Recursively add the first events to the event queue. */ + public void addInitialEvents(ReactorInstance reactor) { + // Add the startup trigger, if exists. + var startup = reactor.getStartupTrigger(); + if (startup != null) eventQ.add(new Event(startup, new Tag(0, 0, false))); + + // Add the initial timer firings, if exist. + for (TimerInstance timer : reactor.timers) { + eventQ.add(new Event(timer, new Tag(timer.getOffset().toNanoSeconds(), 0, false))); + } + + // Recursion + for (var child : reactor.children) { + addInitialEvents(child); + } + } + + /** + * Explore the state space and populate the state space diagram until the specified horizon (i.e. + * the end tag) is reached OR until the event queue is empty. + * + *

As an optimization, if findLoop is true, the algorithm tries to find a loop in the state + * space during exploration. If a loop is found (i.e. a previously encountered state is reached + * again) during exploration, the function returns early. + * + *

TODOs: 1. Handle action with 0 minimum delay. + * + *

Note: This is experimental code which is to be refactored in a future PR. Use with caution. + */ + public void explore(Tag horizon, boolean findLoop) { + // Traverse the main reactor instance recursively to find + // the known initial events (startup and timers' first firings). + // FIXME: It seems that we need to handle shutdown triggers + // separately, because they could break the back loop. + addInitialEvents(this.main); + + Tag previousTag = null; // Tag in the previous loop ITERATION + Tag currentTag = null; // Tag in the current loop ITERATION + StateSpaceNode currentNode = null; + StateSpaceNode previousNode = null; + HashMap uniqueNodes = new HashMap<>(); + boolean stop = true; + if (this.eventQ.size() > 0) { + stop = false; + currentTag = (eventQ.peek()).getTag(); + } + + // A list of reactions invoked at the current logical tag + Set reactionsInvoked; + // A temporary list of reactions processed in the current LOOP ITERATION + Set reactionsTemp; + + while (!stop) { + + // Pop the events from the earliest tag off the event queue. + ArrayList currentEvents = new ArrayList(); + // FIXME: Use stream methods here? + while (eventQ.size() > 0 && eventQ.peek().getTag().compareTo(currentTag) == 0) { + Event e = eventQ.poll(); + currentEvents.add(e); + } + + // Collect all the reactions invoked in this current LOOP ITERATION + // triggered by the earliest events. + // Using a hash set here to make sure the reactions invoked + // are unique. Sometimes multiple events can trigger the same reaction, + // and we do not want to record duplicate reaction invocations. + reactionsTemp = new HashSet(); + for (Event e : currentEvents) { + Set dependentReactions = e.getTrigger().getDependentReactions(); + reactionsTemp.addAll(dependentReactions); + + // If the event is a timer firing, enqueue the next firing. + if (e.getTrigger() instanceof TimerInstance) { + TimerInstance timer = (TimerInstance) e.getTrigger(); + eventQ.add( + new Event( + timer, + new Tag( + e.getTag().timestamp + timer.getPeriod().toNanoSeconds(), + 0, // A time advancement resets microstep to 0. + false))); + } + } + + // For each reaction invoked, compute the new events produced. + for (ReactionInstance reaction : reactionsTemp) { + // Iterate over all the effects produced by this reaction. + // If the effect is a port, obtain the downstream port along + // a connection and enqueue a future event for that port. + // If the effect is an action, enqueue a future event for + // this action. + for (TriggerInstance effect : reaction.effects) { + if (effect instanceof PortInstance) { + + for (SendRange senderRange : ((PortInstance) effect).getDependentPorts()) { + + for (RuntimeRange destinationRange : senderRange.destinations) { + PortInstance downstreamPort = destinationRange.instance; + + // Getting delay from connection + // FIXME: Is there a more concise way to do this? + long delay = 0; + Expression delayExpr = senderRange.connection.getDelay(); + if (delayExpr instanceof Time) { + long interval = ((Time) delayExpr).getInterval(); + String unit = ((Time) delayExpr).getUnit(); + TimeValue timeValue = new TimeValue(interval, TimeUnit.fromName(unit)); + delay = timeValue.toNanoSeconds(); + } + + // Create and enqueue a new event. + Event e = + new Event(downstreamPort, new Tag(currentTag.timestamp + delay, 0, false)); + eventQ.add(e); + } + } + } else if (effect instanceof ActionInstance) { + // Get the minimum delay of this action. + long min_delay = ((ActionInstance) effect).getMinDelay().toNanoSeconds(); + long microstep = 0; + if (min_delay == 0) { + microstep = currentTag.microstep + 1; + } + // Create and enqueue a new event. + Event e = + new Event(effect, new Tag(currentTag.timestamp + min_delay, microstep, false)); + eventQ.add(e); + } + } + } + + // We are at the first iteration. + // Initialize currentNode. + if (previousTag == null) { + //// Now we are done with the node at the previous tag, + //// work on the new node at the current timestamp. + // Copy the reactions in reactionsTemp. + reactionsInvoked = new HashSet(reactionsTemp); + + // Create a new state in the SSD for the current tag, + // add the reactions triggered to the state, + // and add a snapshot of the event queue (with new events + // generated by reaction invocations in the curren tag) + // to the state. + StateSpaceNode node = + new StateSpaceNode( + currentTag, // Current tag + reactionsInvoked, // Reactions invoked at this tag + new ArrayList(eventQ) // A snapshot of the event queue + ); + + // Initialize currentNode. + currentNode = node; + } + // When we advance to a new TIMESTAMP (not a new tag), + // create a new node in the state space diagram + // for everything processed in the previous timestamp. + // This makes sure that the granularity of nodes is + // at the timestamp-level, so that we don't have to + // worry about microsteps. + else if (previousTag != null && currentTag.timestamp > previousTag.timestamp) { + // Whenever we finish a tag, check for loops fist. + // If currentNode matches an existing node in uniqueNodes, + // duplicate is set to the existing node. + StateSpaceNode duplicate; + if (findLoop && (duplicate = uniqueNodes.put(currentNode.hash(), currentNode)) != null) { + + // Mark the loop in the diagram. + loopFound = true; + this.diagram.loopNode = duplicate; + this.diagram.loopNodeNext = currentNode; + this.diagram.tail = previousNode; + // Loop period is the time difference between the 1st time + // the node is reached and the 2nd time the node is reached. + this.diagram.loopPeriod = + this.diagram.loopNodeNext.getTag().timestamp + - this.diagram.loopNode.getTag().timestamp; + this.diagram.addEdge(this.diagram.loopNode, this.diagram.tail); + return; // Exit the while loop early. + } + + // Now we are at a new tag, and a loop is not found, + // add the node to the state space diagram. + // Adding a node to the graph once it is finalized + // because this makes checking duplicate nodes easier. + // We don't have to remove a node from the graph. + this.diagram.addNode(currentNode); + this.diagram.tail = currentNode; // Update the current tail. + + // If the head is not empty, add an edge from the previous state + // to the next state. Otherwise initialize the head to the new node. + if (previousNode != null) { + // System.out.println("--- Add a new edge between " + currentNode + " and " + node); + // this.diagram.addEdge(currentNode, previousNode); // Sink first, then source + if (previousNode != currentNode) this.diagram.addEdge(currentNode, previousNode); + } else this.diagram.head = currentNode; // Initialize the head. + + //// Now we are done with the node at the previous tag, + //// work on the new node at the current timestamp. + // Copy the reactions in reactionsTemp. + reactionsInvoked = new HashSet(reactionsTemp); + + // Create a new state in the SSD for the current tag, + // add the reactions triggered to the state, + // and add a snapshot of the event queue (with new events + // generated by reaction invocations in the curren tag) + // to the state. + StateSpaceNode node = + new StateSpaceNode( + currentTag, // Current tag + reactionsInvoked, // Reactions invoked at this tag + new ArrayList(eventQ) // A snapshot of the event queue + ); + + // Update the previous node. + previousNode = currentNode; + // Update the current node to the new (potentially incomplete) node. + currentNode = node; + } + // Timestamp does not advance because we are processing + // connections with zero delay. + else if (previousTag != null && currentTag.timestamp == previousTag.timestamp) { + // Add reactions explored in the current loop iteration + // to the existing state space node. + currentNode.getReactionsInvoked().addAll(reactionsTemp); + // Update the eventQ snapshot. + currentNode.setEventQcopy(new ArrayList(eventQ)); + } else { + throw new AssertionError("Unreachable"); + } + + // Update the current tag for the next iteration. + if (eventQ.size() > 0) { + previousTag = currentTag; + currentTag = eventQ.peek().getTag(); + } + + // Stop if: + // 1. the event queue is empty, or + // 2. the horizon is reached. + if (eventQ.size() == 0) { + stop = true; + } else if (currentTag.timestamp > horizon.timestamp) { + stop = true; + } + } + + // Check if the last current node is added to the graph yet. + // If not, add it now. + // This could happen when condition (previousTag == null) + // or (previousTag != null + // && currentTag.compareTo(previousTag) > 0) is true and then + // the simulation ends, leaving a new node dangling. + if (previousNode == null || previousNode.getTag().timestamp < currentNode.getTag().timestamp) { + this.diagram.addNode(currentNode); + this.diagram.tail = currentNode; // Update the current tail. + if (previousNode != null) { + this.diagram.addEdge(currentNode, previousNode); + } + } + + // When we exit and we still don't have a head, + // that means there is only one node in the diagram. + // Set the current node as the head. + if (this.diagram.head == null) this.diagram.head = currentNode; + + return; + } +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/StateSpaceNode.java b/core/src/main/java/org/lflang/analyses/statespace/StateSpaceNode.java new file mode 100644 index 0000000000..0061853157 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/StateSpaceNode.java @@ -0,0 +1,101 @@ +package org.lflang.analyses.statespace; + +import java.util.ArrayList; +import java.util.List; +import java.util.Set; +import java.util.stream.Collectors; +import org.lflang.TimeValue; +import org.lflang.generator.ReactionInstance; +import org.lflang.generator.TriggerInstance; + +/** A node in the state space diagram representing a step in the execution of an LF program. */ +public class StateSpaceNode { + + private int index; // Set in StateSpaceDiagram.java + private Tag tag; + private TimeValue time; // Readable representation of tag.timestamp + private Set reactionsInvoked; + private ArrayList eventQcopy; // A snapshot of the eventQ represented as an ArrayList + + public StateSpaceNode( + Tag tag, Set reactionsInvoked, ArrayList eventQcopy) { + this.tag = tag; + this.eventQcopy = eventQcopy; + this.reactionsInvoked = reactionsInvoked; + this.time = TimeValue.fromNanoSeconds(tag.timestamp); + } + + /** Two methods for pretty printing */ + public void display() { + System.out.println("(" + this.time + ", " + reactionsInvoked + ", " + eventQcopy + ")"); + } + + public String toString() { + return "(" + this.time + ", " + reactionsInvoked + ", " + eventQcopy + ")"; + } + + /** + * Generate hash for the node. This hash function is used for checking whether two nodes are + * analogous, meaning that 1) they have the same reactions invoked at their tags, 2) the queued + * events have the same triggers, and 3) the time offsets between future events' tags of one node + * and its tag are the same as the time offsets between future events' tags of the other node and + * the other node's tag. The hash() method is not meant to replace the hashCode() method because + * doing so changes the way nodes are inserted in the state space diagram. + */ + public int hash() { + // Initial value + int result = 17; + + // Generate hash for the reactions invoked. + result = 31 * result + reactionsInvoked.hashCode(); + + // Generate hash for the triggers in the queued events. + List eventNames = + this.eventQcopy.stream() + .map(Event::getTrigger) + .map(TriggerInstance::getFullName) + .collect(Collectors.toList()); + result = 31 * result + eventNames.hashCode(); + + // Generate hash for a list of time differences between future events' tags and + // the current tag. + List timeDiff = + this.eventQcopy.stream() + .map( + e -> { + return e.getTag().timestamp - this.tag.timestamp; + }) + .collect(Collectors.toList()); + result = 31 * result + timeDiff.hashCode(); + + return result; + } + + public int getIndex() { + return index; + } + + public void setIndex(int i) { + index = i; + } + + public Tag getTag() { + return tag; + } + + public TimeValue getTime() { + return time; + } + + public Set getReactionsInvoked() { + return reactionsInvoked; + } + + public ArrayList getEventQcopy() { + return eventQcopy; + } + + public void setEventQcopy(ArrayList list) { + eventQcopy = list; + } +} diff --git a/core/src/main/java/org/lflang/analyses/statespace/Tag.java b/core/src/main/java/org/lflang/analyses/statespace/Tag.java new file mode 100644 index 0000000000..f62dde6c32 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/statespace/Tag.java @@ -0,0 +1,63 @@ +package org.lflang.analyses.statespace; + +import org.lflang.TimeValue; + +/** + * Class representing a logical time tag, which is a pair that consists of a timestamp (type long) + * and a microstep (type long). + */ +public class Tag implements Comparable { + + public final long timestamp; + public final long microstep; + public final boolean forever; // Whether the tag is FOREVER into the future. + + public Tag(long timestamp, long microstep, boolean forever) { + this.timestamp = timestamp; + this.microstep = microstep; + this.forever = forever; + } + + @Override + public int compareTo(Tag t) { + // If one tag is forever, and the other is not, + // then forever tag is later. If both tags are + // forever, then they are equal. + if (this.forever && !t.forever) return 1; + else if (!this.forever && t.forever) return -1; + else if (this.forever && t.forever) return 0; + + // Compare the timestamps if they are not equal. + if (this.timestamp != t.timestamp) { + if (this.timestamp > t.timestamp) return 1; + else if (this.timestamp < t.timestamp) return -1; + else return 0; + } + + // Otherwise, compare the microsteps. + if (this.microstep > t.microstep) return 1; + else if (this.microstep < t.microstep) return -1; + else return 0; + } + + @Override + public boolean equals(Object o) { + if (this == o) return true; + if (o instanceof Tag) { + Tag t = (Tag) o; + if (this.timestamp == t.timestamp + && this.microstep == t.microstep + && this.forever == t.forever) return true; + } + return false; + } + + @Override + public String toString() { + if (this.forever) return "(FOREVER, " + this.microstep + ")"; + else { + TimeValue time = TimeValue.fromNanoSeconds(this.timestamp); + return "(" + time + ", " + this.microstep + ")"; + } + } +} diff --git a/core/src/main/java/org/lflang/analyses/uclid/MTLVisitor.java b/core/src/main/java/org/lflang/analyses/uclid/MTLVisitor.java new file mode 100644 index 0000000000..1aef6fe554 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/uclid/MTLVisitor.java @@ -0,0 +1,657 @@ +/************* + * Copyright (c) 2021, The University of California at Berkeley. + * + * 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. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 COPYRIGHT HOLDER OR CONTRIBUTORS 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. + ***************/ + +package org.lflang.analyses.uclid; + +import org.lflang.TimeUnit; +import org.lflang.TimeValue; +import org.lflang.analyses.uclid.UclidGenerator.Tactic; +import org.lflang.dsl.MTLParser; +import org.lflang.dsl.MTLParserBaseVisitor; +import org.lflang.generator.CodeBuilder; + +/** (EXPERIMENTAL) Transpiler from an MTL specification to a Uclid axiom. */ +public class MTLVisitor extends MTLParserBaseVisitor { + + //////////////////////////////////////////// + //// Protected fields + + /** The main place to put generated code. */ + protected CodeBuilder code = new CodeBuilder(); + + /** Tactic to be used to prove the property. */ + protected Tactic tactic; + + /** Time horizon (in nanoseconds) of the property */ + protected long horizon = 0; + + // Constructor + public MTLVisitor(Tactic tactic) { + this.tactic = tactic; + } + + //////////////////////////////////////////// + //// Public methods + public String visitMtl( + MTLParser.MtlContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon) { + + return visitEquivalence(ctx.equivalence(), prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + public String visitEquivalence( + MTLParser.EquivalenceContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + if (ctx.right == null) { + return visitImplication(ctx.left, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + return "(" + + visitImplication(ctx.left, prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + " <==> " + + "(" + + visitImplication(ctx.right, prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")"; + } + + public String visitImplication( + MTLParser.ImplicationContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + if (ctx.right == null) { + return visitDisjunction(ctx.left, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + return "(" + + visitDisjunction(ctx.left, prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + " ==> " + + "(" + + visitDisjunction(ctx.right, prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")"; + } + + public String visitDisjunction( + MTLParser.DisjunctionContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String str = ""; + for (int i = 0; i < ctx.terms.size(); i++) { + str += + "(" + + visitConjunction(ctx.terms.get(i), prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + (i == ctx.terms.size() - 1 ? "" : "||"); + } + return str; + } + + public String visitConjunction( + MTLParser.ConjunctionContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String str = ""; + for (int i = 0; i < ctx.terms.size(); i++) { + str += + "(" + + visitUntil( + (MTLParser.UntilContext) ctx.terms.get(i), + prefixIdx, + QFIdx, + prevPrefixIdx, + horizon) + + ")" + + (i == ctx.terms.size() - 1 ? "" : "&&"); + } + return str; + } + + // A custom dispatch function + public String _visitUnaryOp( + MTLParser.UnaryOpContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + // FIXME: Is there a more "antlr" way to do dispatch here? + if (ctx instanceof MTLParser.NoUnaryOpContext _ctx) { + return visitNoUnaryOp(_ctx, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + if (ctx instanceof MTLParser.NegationContext _ctx) { + return visitNegation(_ctx, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + if (ctx instanceof MTLParser.NextContext _ctx) { + return visitNext(_ctx, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + if (ctx instanceof MTLParser.GloballyContext _ctx) { + return visitGlobally(_ctx, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + if (ctx instanceof MTLParser.FinallyContext _ctx) { + return visitFinally(_ctx, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + // FIXME: Throw an exception. + return ""; + } + + public String visitUntil( + MTLParser.UntilContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon) { + + // If right is null, continue recursion. + if (ctx.right == null) { + return _visitUnaryOp(ctx.left, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + String end; + if (this.tactic == Tactic.INDUCTION) { + end = "(" + prefixIdx + " + CT)"; + } else { + end = "END"; + } + + // Otherwise, create the Until formula. + // Check if the time interval is a range or a singleton. + long lowerBoundNanoSec = getNanoSecFromIntervalContext(ctx.timeInterval, false); + long upperBoundNanoSec = getNanoSecFromIntervalContext(ctx.timeInterval, true); + long currentHorizon = horizon + upperBoundNanoSec; + if (currentHorizon > this.horizon) this.horizon = currentHorizon; + String timePredicate = + generateTimePredicate( + ctx.timeInterval, lowerBoundNanoSec, upperBoundNanoSec, "j" + QFIdx, prefixIdx); + + return "finite_exists " + + "(" + + "j" + + QFIdx + + " : integer) in indices :: " + + "j" + + QFIdx + + " >= " + + prefixIdx + + " && " + + "j" + + QFIdx + + " <= " + + end + + " && " + + "!" + + "isNULL" + + "(" + + "j" + + QFIdx + + ")" + + " && " + + "(" + + _visitUnaryOp(ctx.right, ("j" + QFIdx), QFIdx + 1, prefixIdx, currentHorizon) + + ")" + + " && " + + "(" + + "\n" + + "// Time Predicate\n" + + timePredicate + + "\n" + + ")" + + " && " + + "(" + + "finite_forall " + + "(" + + "i" + + QFIdx + + " : integer) in indices :: " + + "(" + + "i" + + QFIdx + + " >= " + + prefixIdx + + " && " + + "i" + + QFIdx + + " < " + + "j" + + QFIdx + + ")" + + " ==> " + + "(" + + _visitUnaryOp(ctx.left, ("i" + QFIdx), QFIdx + 1, ("j" + QFIdx), currentHorizon) + + ")" + + ")"; + } + + public String visitNoUnaryOp( + MTLParser.NoUnaryOpContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + return visitPrimary(ctx.formula, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + public String visitNegation( + MTLParser.NegationContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + return "!(" + visitPrimary(ctx.formula, prefixIdx, QFIdx, prevPrefixIdx, horizon) + ")"; + } + + public String visitNext( + MTLParser.NextContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon) { + // FIXME: Horizon needs to advance! + return visitPrimary(ctx.formula, ("(" + prefixIdx + "+1)"), QFIdx, prevPrefixIdx, horizon); + } + + public String visitGlobally( + MTLParser.GloballyContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String end; + if (this.tactic == Tactic.INDUCTION) { + end = "(" + prefixIdx + " + CT)"; + } else { + end = "END"; + } + + long lowerBoundNanoSec = getNanoSecFromIntervalContext(ctx.timeInterval, false); + long upperBoundNanoSec = getNanoSecFromIntervalContext(ctx.timeInterval, true); + long currentHorizon = horizon + upperBoundNanoSec; + if (currentHorizon > this.horizon) this.horizon = currentHorizon; + String timePredicate = + generateTimePredicate( + ctx.timeInterval, lowerBoundNanoSec, upperBoundNanoSec, "j" + QFIdx, prefixIdx); + return "(" + + "finite_forall " + + "(" + + "j" + + QFIdx + + " : integer) in indices :: " + + "(" + + "j" + + QFIdx + + " >= " + + prefixIdx + + " && " + + "j" + + QFIdx + + " <= " + + end + + " && " + + "!" + + "isNULL" + + "(" + + "j" + + QFIdx + + ")" + + " && " + + "(" + + "\n" + + "// Time Predicate\n" + + timePredicate + + "\n" + + ")" + + ")" + + " ==> " + + "(" + + visitPrimary(ctx.formula, ("j" + QFIdx), QFIdx + 1, prefixIdx, currentHorizon) + + ")" + + ")"; + } + + public String visitFinally( + MTLParser.FinallyContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String end; + if (this.tactic == Tactic.INDUCTION) { + end = "(" + prefixIdx + " + CT)"; + } else { + end = "END"; + } + + long lowerBoundNanoSec = getNanoSecFromIntervalContext(ctx.timeInterval, false); + long upperBoundNanoSec = getNanoSecFromIntervalContext(ctx.timeInterval, true); + long currentHorizon = horizon + upperBoundNanoSec; + if (currentHorizon > this.horizon) this.horizon = currentHorizon; + String timePredicate = + generateTimePredicate( + ctx.timeInterval, lowerBoundNanoSec, upperBoundNanoSec, "j" + QFIdx, prefixIdx); + return "finite_exists " + + "(" + + "j" + + QFIdx + + " : integer) in indices :: " + + "j" + + QFIdx + + " >= " + + prefixIdx + + " && " + + "j" + + QFIdx + + " <= " + + end + + " && " + + "!" + + "isNULL" + + "(" + + "j" + + QFIdx + + ")" + + " && " + + "(" + + visitPrimary(ctx.formula, ("j" + QFIdx), QFIdx + 1, prefixIdx, currentHorizon) + + ")" + + " && " + + "(" + + "\n" + + "// Time Predicate\n" + + timePredicate + + "\n" + + ")"; + } + + public String visitPrimary( + MTLParser.PrimaryContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + if (ctx.atom != null) + return visitAtomicProp(ctx.atom, prefixIdx, QFIdx, prevPrefixIdx, horizon); + else if (ctx.id != null) { + // Check if the ID is a reaction. + // FIXME: Not robust. + if (ctx.id.getText().contains("_reaction_")) { + return ctx.id.getText() + "(" + "rxn(" + prefixIdx + ")" + ")"; + } else if (ctx.id.getText().contains("_is_present")) { + return ctx.id.getText() + "(" + "t(" + prefixIdx + ")" + ")"; + } else { + return ctx.id.getText() + "(" + "s(" + prefixIdx + ")" + ")"; + } + } else return visitMtl(ctx.formula, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + public String visitAtomicProp( + MTLParser.AtomicPropContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + if (ctx.primitive != null) return ctx.primitive.getText(); + else + return visitExpr(ctx.left, prefixIdx, QFIdx, prevPrefixIdx, horizon) + + " " + + ctx.op.getText() + + " " + + visitExpr(ctx.right, prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + public String visitExpr( + MTLParser.ExprContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon) { + + if (ctx.ID() != null) return ctx.ID().getText() + "(" + "s(" + prefixIdx + ")" + ")"; + else if (ctx.INTEGER() != null) return ctx.INTEGER().getText(); + else return visitSum(ctx.sum(), prefixIdx, QFIdx, prevPrefixIdx, horizon); + } + + public String visitSum( + MTLParser.SumContext ctx, String prefixIdx, int QFIdx, String prevPrefixIdx, long horizon) { + + String str = ""; + for (int i = 0; i < ctx.terms.size(); i++) { + str += + "(" + + visitDifference(ctx.terms.get(i), prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + (i == ctx.terms.size() - 1 ? "" : "+"); + } + return str; + } + + public String visitDifference( + MTLParser.DifferenceContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String str = ""; + for (int i = 0; i < ctx.terms.size(); i++) { + str += + "(" + + visitProduct(ctx.terms.get(i), prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + (i == ctx.terms.size() - 1 ? "" : "-"); + } + return str; + } + + public String visitProduct( + MTLParser.ProductContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String str = ""; + for (int i = 0; i < ctx.terms.size(); i++) { + str += + "(" + + visitQuotient(ctx.terms.get(i), prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + (i == ctx.terms.size() - 1 ? "" : "*"); + } + return str; + } + + public String visitQuotient( + MTLParser.QuotientContext ctx, + String prefixIdx, + int QFIdx, + String prevPrefixIdx, + long horizon) { + + String str = ""; + for (int i = 0; i < ctx.terms.size(); i++) { + str += + "(" + + visitExpr(ctx.terms.get(i), prefixIdx, QFIdx, prevPrefixIdx, horizon) + + ")" + + (i == ctx.terms.size() - 1 ? "" : "/"); + } + return str; + } + + /////////////////////////////////////// + //// Private methods + + /** + * Return a time value in nanoseconds from an IntervalContext. + * + * @param ctx + * @param getUpper + * @return + */ + private long getNanoSecFromIntervalContext(MTLParser.IntervalContext ctx, boolean getUpper) { + // If we have a singleton, the return value is the same regardless of getUpper. + if (ctx instanceof MTLParser.SingletonContext) { + MTLParser.SingletonContext singletonCtx = (MTLParser.SingletonContext) ctx; + String timeInstantValue = singletonCtx.instant.value.getText(); + String timeInstantUnit = ""; + long timeInstantNanoSec = 0; + if (!timeInstantValue.equals("0")) { + timeInstantUnit = singletonCtx.instant.unit.getText(); + TimeValue timeValue = + new TimeValue(Integer.valueOf(timeInstantValue), TimeUnit.fromName(timeInstantUnit)); + timeInstantNanoSec = timeValue.toNanoSeconds(); + } + return timeInstantNanoSec; + } + + MTLParser.RangeContext rangeCtx = (MTLParser.RangeContext) ctx; + if (!getUpper) { + String lowerBoundTimeValue = rangeCtx.lowerbound.value.getText(); + String lowerBoundTimeUnit = ""; + long lowerBoundNanoSec = 0; + if (!lowerBoundTimeValue.equals("0")) { + lowerBoundTimeUnit = rangeCtx.lowerbound.unit.getText(); + TimeValue lowerTimeValue = + new TimeValue( + Integer.valueOf(lowerBoundTimeValue), TimeUnit.fromName(lowerBoundTimeUnit)); + lowerBoundNanoSec = lowerTimeValue.toNanoSeconds(); + } + return lowerBoundNanoSec; + } else { + String upperBoundTimeValue = rangeCtx.upperbound.value.getText(); + String upperBoundTimeUnit = ""; + long upperBoundNanoSec = 0; + if (!upperBoundTimeValue.equals("0")) { + upperBoundTimeUnit = rangeCtx.upperbound.unit.getText(); + TimeValue upperTimeValue = + new TimeValue( + Integer.valueOf(upperBoundTimeValue), TimeUnit.fromName(upperBoundTimeUnit)); + upperBoundNanoSec = upperTimeValue.toNanoSeconds(); + } + return upperBoundNanoSec; + } + } + + /** + * Generate a time predicate from a range. + * + * @param ctx + * @param lowerBoundNanoSec The lowerbound of the time interval (in nanoseconds) in an MTL formula + * @param upperBoundNanoSec The upperbound of the time interval (in nanoseconds) in an MTL formula + * @return + */ + private String generateTimePredicate( + MTLParser.IntervalContext ctx, + long lowerBoundNanoSec, + long upperBoundNanoSec, + String prefixIdx, + String prevPrefixIdx) { + String timePredicate = ""; + + if (ctx instanceof MTLParser.SingletonContext) { + MTLParser.SingletonContext singletonCtx = (MTLParser.SingletonContext) ctx; + timePredicate += + "tag_same(g(" + + prefixIdx + + "), " + + "tag_delay(g(" + + prevPrefixIdx + + "), " + + upperBoundNanoSec + + "))"; + } else { + // Since MTL doesn't include microsteps, we only compare timestamps here. + MTLParser.RangeContext rangeCtx = (MTLParser.RangeContext) ctx; + timePredicate += "("; + if (rangeCtx.LBRACKET() != null) { + timePredicate += + "pi1(g(" + + prefixIdx + + "))" + + " >= " + + "(" + + "pi1(g(" + + prevPrefixIdx + + "))" + + " + " + + lowerBoundNanoSec + + ")"; + } else { + timePredicate += + "pi1(g(" + + prefixIdx + + "))" + + " > " + + "(" + + "pi1(g(" + + prevPrefixIdx + + "))" + + " + " + + lowerBoundNanoSec + + ")"; + } + timePredicate += ") && ("; + if (rangeCtx.RBRACKET() != null) { + timePredicate += + "pi1(g(" + + prefixIdx + + "))" + + " <= " + + "(" + + "pi1(g(" + + prevPrefixIdx + + "))" + + " + " + + upperBoundNanoSec + + ")"; + } else { + timePredicate += + "pi1(g(" + + prefixIdx + + "))" + + " < " + + "(" + + "pi1(g(" + + prevPrefixIdx + + "))" + + " + " + + upperBoundNanoSec + + ")"; + } + timePredicate += ")"; + } + + return timePredicate; + } + + /** Get the time horizon (in nanoseconds) of the property. */ + public long getHorizon() { + return this.horizon; + } +} diff --git a/core/src/main/java/org/lflang/analyses/uclid/UclidGenerator.java b/core/src/main/java/org/lflang/analyses/uclid/UclidGenerator.java new file mode 100644 index 0000000000..c563356edf --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/uclid/UclidGenerator.java @@ -0,0 +1,1747 @@ +/************* + * Copyright (c) 2021, The University of California at Berkeley. + * + * 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. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 COPYRIGHT HOLDER OR CONTRIBUTORS 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. + ***************/ + +package org.lflang.analyses.uclid; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import org.antlr.v4.runtime.CharStreams; +import org.antlr.v4.runtime.CommonTokenStream; +import org.eclipse.emf.ecore.resource.Resource; +import org.lflang.Target; +import org.lflang.TimeUnit; +import org.lflang.TimeValue; +import org.lflang.analyses.c.AstUtils; +import org.lflang.analyses.c.BuildAstParseTreeVisitor; +import org.lflang.analyses.c.CAst; +import org.lflang.analyses.c.CToUclidVisitor; +import org.lflang.analyses.c.IfNormalFormAstVisitor; +import org.lflang.analyses.c.VariablePrecedenceVisitor; +import org.lflang.analyses.statespace.StateSpaceDiagram; +import org.lflang.analyses.statespace.StateSpaceExplorer; +import org.lflang.analyses.statespace.StateSpaceNode; +import org.lflang.analyses.statespace.Tag; +import org.lflang.ast.ASTUtils; +import org.lflang.dsl.CLexer; +import org.lflang.dsl.CParser; +import org.lflang.dsl.CParser.BlockItemListContext; +import org.lflang.dsl.MTLLexer; +import org.lflang.dsl.MTLParser; +import org.lflang.dsl.MTLParser.MtlContext; +import org.lflang.generator.ActionInstance; +import org.lflang.generator.CodeBuilder; +import org.lflang.generator.GeneratorBase; +import org.lflang.generator.LFGeneratorContext; +import org.lflang.generator.NamedInstance; +import org.lflang.generator.PortInstance; +import org.lflang.generator.ReactionInstance; +import org.lflang.generator.ReactorInstance; +import org.lflang.generator.RuntimeRange; +import org.lflang.generator.SendRange; +import org.lflang.generator.StateVariableInstance; +import org.lflang.generator.TargetTypes; +import org.lflang.generator.TimerInstance; +import org.lflang.generator.TriggerInstance; +import org.lflang.lf.AttrParm; +import org.lflang.lf.Attribute; +import org.lflang.lf.Connection; +import org.lflang.lf.Expression; +import org.lflang.lf.Time; +import org.lflang.util.StringUtil; + +/** (EXPERIMENTAL) Generator for Uclid5 models. */ +public class UclidGenerator extends GeneratorBase { + + //////////////////////////////////////////// + //// Public fields + /** A list of reaction runtime instances. */ + public List reactionInstances = + new ArrayList(); + + /** A list of action instances */ + public List actionInstances = new ArrayList(); + + /** Joint lists of the lists above. */ + public List triggerInstances; // Triggers = ports + actions + timers + + public List namedInstances; // Named instances = triggers + state variables + + /** A list of paths to the uclid files generated */ + public List generatedFiles = new ArrayList<>(); + + public Map expectations = new HashMap<>(); + + /** The directory where the generated files are placed */ + public Path outputDir; + + /** A runner for the generated Uclid files */ + public UclidRunner runner; + + /** Completeness threshold */ + public int CT = 0; + + //////////////////////////////////////////// + //// Private fields + /** A list of reactor runtime instances. */ + private List reactorInstances = new ArrayList(); + + /** State variables in the system */ + private List stateVariables = new ArrayList(); + + /** A list of input port instances */ + private List inputInstances = new ArrayList(); + + /** A list of output port instances */ + private List outputInstances = new ArrayList(); + + /** A list of input AND output port instances */ + private List portInstances = new ArrayList(); + + /** A list of timer instances */ + private List timerInstances = new ArrayList(); + + /** A list of MTL properties represented in Attributes. */ + private List properties; + + /** The main place to put generated code. */ + private CodeBuilder code = new CodeBuilder(); + + /** Strings from the property attribute */ + private String name; + + /** + * A tactic used to verify properties. Currently, only BMC (bounded model checking) is functional. + * FIXME: For a future version that supports multiple tactics, the tactics should be stored in a + * list. + */ + enum Tactic { + BMC, + INDUCTION + } + + private Tactic tactic; + + /** Safety MTL property to be verified */ + private String spec; + + /** A property's ground truth value, for debugging the verifier */ + private String expect; + + /** + * The horizon (the total time interval required for evaluating an MTL property, which is derived + * from the MTL spec), the completeness threshold (CT) (the number of transitions required for + * evaluating the FOL spec in the trace), and the transpiled FOL spec. + */ + private long horizon = 0; // in nanoseconds + + /** First-Order Logic formula matching the Safety MTL property */ + private String FOLSpec = ""; + + /** Maximum CT supported. This is a hardcoded value. */ + private static final int CT_MAX_SUPPORTED = 100; + + /** + * If true, use logical time-based semantics; otherwise, use event-based semantics, as described + * in Sirjani et. al (2020). This is currently always false and serves as a placeholder for a + * future version that supports logical time-based semantics. + */ + private boolean logicalTimeBased = false; + + /** Constructor */ + public UclidGenerator(LFGeneratorContext context, List properties) { + super(context); + this.properties = properties; + this.runner = new UclidRunner(this); + } + + //////////////////////////////////////////////////////////// + //// Public methods + public void doGenerate(Resource resource, LFGeneratorContext context) { + + // Reuse parts of doGenerate() from GeneratorBase. + super.printInfo(context.getMode()); + ASTUtils.setMainName(context.getFileConfig().resource, context.getFileConfig().name); + super.createMainInstantiation(); + super.setReactorsAndInstantiationGraph(context.getMode()); + + // Create the main reactor instance if there is a main reactor. + this.main = + ASTUtils.createMainReactorInstance(mainDef, reactors, messageReporter, targetConfig); + + // Extract information from the named instances. + populateDataStructures(); + + // Create the src-gen directory + setupDirectories(); + + // Generate a Uclid model for each property. + for (Attribute prop : this.properties) { + this.name = + StringUtil.removeQuotes( + prop.getAttrParms().stream() + .filter(attr -> attr.getName().equals("name")) + .findFirst() + .get() + .getValue()); + String tacticStr = + StringUtil.removeQuotes( + prop.getAttrParms().stream() + .filter(attr -> attr.getName().equals("tactic")) + .findFirst() + .get() + .getValue()); + if (tacticStr.equals("bmc")) this.tactic = Tactic.BMC; + this.spec = + StringUtil.removeQuotes( + prop.getAttrParms().stream() + .filter(attr -> attr.getName().equals("spec")) + .findFirst() + .get() + .getValue()); + + processMTLSpec(); + + Optional CTAttr = + prop.getAttrParms().stream().filter(attr -> attr.getName().equals("CT")).findFirst(); + if (CTAttr.isPresent()) { + this.CT = Integer.parseInt(CTAttr.get().getValue()); + } else { + computeCT(); + } + // For automating data collection, print the CT to stderr. + System.err.println("CT: " + this.CT); + if (this.CT > CT_MAX_SUPPORTED) { + System.out.println( + "ERROR: The maximum steps supported is " + + CT_MAX_SUPPORTED + + " but checking this property requires " + + this.CT + + " steps. " + + "This property will NOT be checked."); + continue; + } + + Optional ExpectAttr = + prop.getAttrParms().stream().filter(attr -> attr.getName().equals("expect")).findFirst(); + if (ExpectAttr.isPresent()) this.expect = ExpectAttr.get().getValue(); + + generateUclidFile(); + } + } + + //////////////////////////////////////////////////////////// + //// Protected methods + + /** Generate the Uclid model. */ + protected void generateUclidFile() { + try { + // Generate main.ucl and print to file + code = new CodeBuilder(); + Path file = this.outputDir.resolve(this.tactic + "_" + this.name + ".ucl"); + String filename = file.toString(); + generateUclidCode(); + code.writeToFile(filename); + this.generatedFiles.add(file); + if (this.expect != null) this.expectations.put(file, this.expect); + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + /** The main function that generates Uclid code. */ + protected void generateUclidCode() { + code.pr( + String.join( + "\n", + "/*******************************", + " * Auto-generated UCLID5 model *", + " ******************************/")); + + code.pr("module main {"); + code.indent(); + + // Timing semantics + generateTimingSemantics(); + + // Trace definition + generateTraceDefinition(); + + // Reaction IDs and state variables + generateReactionIdsAndStateVars(); + + // Reactor semantics + generateReactorSemantics(); + + // Triggers and reactions + generateTriggersAndReactions(); + + // Initial Condition + generateInitialConditions(); + + // Reaction bodies + generateReactionAxioms(); + + // Properties + generateProperty(); + + // Control block + generateControlBlock(); + + code.unindent(); + code.pr("}"); + } + + /** Macros for timing semantics */ + protected void generateTimingSemantics() { + code.pr( + String.join( + "\n", + "/*******************************", + " * Time and Related Operations *", + " ******************************/", + "type timestamp_t = integer; // The unit is nanoseconds", + "type microstep_t = integer;", + "type tag_t = {", + " timestamp_t,", + " microstep_t", + "};", + "type interval_t = tag_t;", + "", + "// Projection macros", + "define pi1(t : tag_t) : timestamp_t = t._1; // Get timestamp from tag", + "define pi2(t : tag_t) : microstep_t = t._2; // Get microstep from tag", + "", + "// Interval constructor", + "define zero() : interval_t", + "= {0, 0};", + "define startup() : interval_t", + "= zero();", + "define mstep() : interval_t", + "= {0, 1};", + "define nsec(t : integer) : interval_t", + "= {t, 0};", + "define usec(t : integer) : interval_t", + "= {t * 1000, 0};", + "define msec(t : integer) : interval_t", + "= {t * 1000000, 0};", + "define sec(t : integer) : interval_t", + "= {t * 1000000000, 0};", + "define inf() : interval_t", + "= {-1, 0};", + "", + "// Helper function", + "define isInf(i : interval_t) : boolean", + "= pi1(i) < 0;", + "", + "// Tag comparison", + "define tag_later(t1 : tag_t, t2 : tag_t) : boolean", + "= pi1(t1) > pi1(t2)", + " || (pi1(t1) == pi1(t2) && pi2(t1) > pi2(t2))", + " || (isInf(t1) && !isInf(t2));", + "", + "define tag_same(t1 : tag_t, t2 : tag_t) : boolean", + "= t1 == t2;", + "", + "define tag_earlier(t1 : tag_t, t2 : tag_t) : boolean", + "= pi1(t1) < pi1(t2)", + " || (pi1(t1) == pi1(t2) && pi2(t1) < pi2(t2))", + " || (!isInf(t1) && isInf(t2));", + "", + "// Used for incrementing a tag through an action", + "define tag_schedule(t : tag_t, i : integer) : tag_t", + "= if (i == 0) then { pi1(t), pi2(t)+1 } else { pi1(t)+i, 0 };", + "", + "// Used for incrementing a tag along a connection", + "define tag_delay(t : tag_t, i : integer) : tag_t", + "= if (i == 0) then { pi1(t), pi2(t) } else { pi1(t)+i, 0 };", + "", + "// Only consider timestamp for now.", + "define tag_diff(t1, t2: tag_t) : interval_t", + "= if (!isInf(t1) && !isInf(t2))", + " then { pi1(t1) - pi1(t2), pi2(t1) - pi2(t2) }", + " else inf();", + "\n")); + } + + /** Macros, type definitions, and variable declarations for trace (path) */ + protected void generateTraceDefinition() { + //// Why do we have a padding at the end of the trace? + // + // To handle bounded traces for a potentially unbounded execution + // (due to, for example, timers or systems forming a loop), + // we need to let certain axioms "terminate" the execution and + // put any "spilled-over" states in the trace padding. + // + // For example, an axiom could say "if a reaction is triggered + // at step i, it schedules an action that appears 1 sec later + // in some future step." Assuming our completeness threshold is 10, + // this axiom can block the model (i.e. returns TRIVIALLY true) + // at step 10 because there are not any more steps in the bounded trace. + // To avoid this, a padding of the size of the number of reactions + // is added to the trace. In addition, an antecedent of the form + // "i >= START && i <= END" is added to all the axioms. The padding + // will store all the spilled-over states in order to prevent + // model blocking. + int traceEndIndex = this.CT + this.reactionInstances.size(); + + // Define various constants. + code.pr( + String.join( + "\n", + "/********************", + " * Trace Definition *", + " *******************/", + "const START : integer = 0; // The start index of the trace.", + "const END : integer = " + + String.valueOf(this.CT) + + "; // The end index of the trace (without padding)", + "const END_TRACE : integer = " + + String.valueOf(traceEndIndex) + + "; // The end index of the trace with padding", + "\n")); + + // Define trace indices as a group, + // so that we can use finite quantifiers. + code.pr("group indices : integer = {"); + code.indent(); + String indices = ""; + for (int i = 0; i <= traceEndIndex; i++) { + indices += String.valueOf(i) + (i == traceEndIndex ? "" : ", "); + } + code.pr(indices); + code.unindent(); + code.pr("};\n\n"); + + // Define step, event, and trace types. + code.pr( + String.join( + "\n", + "// Define step and event types.", + "type step_t = integer;", + "type event_t = { rxn_t, tag_t, state_t, trigger_t, sched_t, payload_t };", + "", + "// Create a bounded trace with length " + String.valueOf(this.CT))); + code.pr("// Potentially unbounded trace, we bound this later."); + code.pr("type trace_t = [integer]event_t;"); + + // Declare start time and trace. + code.pr( + String.join( + "\n", + "// Declare start time.", + "var start_time : timestamp_t;", + "", + "// Declare trace.", + "var trace : trace_t;")); + + // Start generating helper macros. + code.pr(String.join("\n", "/*****************", " * Helper Macros *", " ****************/")); + + // Define a getter for uclid arrays. + String initialReactions = ""; + if (this.reactionInstances.size() > 0) { + initialReactions = "false, ".repeat(this.reactionInstances.size()); + initialReactions = initialReactions.substring(0, initialReactions.length() - 2); + } else { + // Initialize a dummy variable just to make the code compile. + initialReactions = "false"; + } + initialReactions = "{" + initialReactions + "}"; + String initialStates = ""; + if (this.namedInstances.size() > 0) { + initialStates = "0, ".repeat(this.namedInstances.size()); + initialStates = initialStates.substring(0, initialStates.length() - 2); + } else { + // Initialize a dummy variable just to make the code compile. + initialStates = "0"; + } + String initialTriggerPresence = ""; + if (this.triggerInstances.size() > 0) { + initialTriggerPresence = "false, ".repeat(this.triggerInstances.size()); + initialTriggerPresence = + initialTriggerPresence.substring(0, initialTriggerPresence.length() - 2); + } else { + // Initialize a dummy variable just to make the code compile. + initialTriggerPresence = "false"; + } + String initialActionsScheduled = ""; + if (this.actionInstances.size() > 0) { + initialActionsScheduled = "false, ".repeat(this.actionInstances.size()); + initialActionsScheduled = + initialActionsScheduled.substring(0, initialActionsScheduled.length() - 2); + } else { + // Initialize a dummy variable just to make the code compile. + initialActionsScheduled = "false"; + } + String initialActionsScheduledPayload = ""; + if (this.actionInstances.size() > 0) { + initialActionsScheduledPayload = "0, ".repeat(this.actionInstances.size()); + initialActionsScheduledPayload = + initialActionsScheduledPayload.substring(0, initialActionsScheduledPayload.length() - 2); + } else { + // Initialize a dummy variable just to make the code compile. + initialActionsScheduledPayload = "0"; + } + code.pr("// Helper macro that returns an element based on index."); + code.pr("define get(tr : trace_t, i : step_t) : event_t ="); + code.pr("if (i >= START && i <= END_TRACE) then tr[i] else"); + code.pr( + "{ " + + initialReactions + + ", inf(), { " + + initialStates + + " }, { " + + initialTriggerPresence + + " }, {" + + initialActionsScheduled + + " }, {" + + initialActionsScheduledPayload + + "} };"); + + // Define an event getter from the trace. + code.pr( + String.join( + "\n", + "define elem(i : step_t) : event_t", + "= get(trace, i);", + "", + "// projection macros", + "define rxn (i : step_t) : rxn_t = elem(i)._1;", + "define g (i : step_t) : tag_t = elem(i)._2;", + "define s (i : step_t) : state_t = elem(i)._3;", + "define t (i : step_t) : trigger_t = elem(i)._4;", + "define d (i : step_t) : sched_t = elem(i)._5;", + "define pl (i : step_t) : payload_t = elem(i)._6;", + "define isNULL (i : step_t) : boolean = rxn(i) == " + initialReactions + ";")); + } + + /** Type definitions for runtime reaction Ids and state variables */ + protected void generateReactionIdsAndStateVars() { + // Encode the components and the logical delays + // present in a reactor system. + code.pr( + String.join( + "\n", + "/**********************************", + " * Reaction IDs & State Variables *", + " *********************************/", + "", + "//////////////////////////", + "// Application Specific")); + + // Enumerate over all reactions. + code.pr(String.join("\n", "// Reactions", "type rxn_t = {")); + code.indent(); + for (var i = 0; i < this.reactionInstances.size(); i++) { + // Print a list of reaction IDs. + // Add a comma if not last. + code.pr( + "boolean" + + ((i == this.reactionInstances.size() - 1) ? "" : ",") + + "\t// " + + this.reactionInstances.get(i)); + } + code.unindent(); + code.pr("};\n"); + + // Generate projection macros. + code.pr("// Reaction projection macros"); + for (var i = 0; i < this.reactionInstances.size(); i++) { + code.pr( + "define " + + this.reactionInstances.get(i).getReaction().getFullNameWithJoiner("_") + + "(n : rxn_t) : boolean = n._" + + (i + 1) + + ";"); + } + code.pr("\n"); // Newline + + // State variables and triggers + // FIXME: expand to data types other than integer + code.pr("// State variables and triggers"); + code.pr("type state_t = {"); + code.indent(); + if (this.namedInstances.size() > 0) { + for (var i = 0; i < this.namedInstances.size(); i++) { + code.pr( + "integer" + + ((i == this.namedInstances.size() - 1) ? "" : ",") + + "\t// " + + this.namedInstances.get(i)); + } + } else { + code.pr( + String.join( + "\n", + "// There are no ports or state variables.", + "// Insert a dummy integer to make the model compile.", + "integer")); + } + code.unindent(); + code.pr("};"); + code.pr("// State variable projection macros"); + for (var i = 0; i < this.namedInstances.size(); i++) { + code.pr( + "define " + + this.namedInstances.get(i).getFullNameWithJoiner("_") + + "(s : state_t) : integer = s._" + + (i + 1) + + ";"); + } + code.pr("\n"); // Newline + + // A boolean tuple indicating whether triggers are present. + code.pr("// A boolean tuple indicating whether triggers are present."); + code.pr("type trigger_t = {"); + code.indent(); + if (this.triggerInstances.size() > 0) { + for (var i = 0; i < this.triggerInstances.size(); i++) { + code.pr( + "boolean" + + ((i == this.triggerInstances.size() - 1) ? "" : ",") + + "\t// " + + this.triggerInstances.get(i)); + } + } else { + code.pr( + String.join( + "\n", + "// There are no triggers.", + "// Insert a dummy boolean to make the model compile.", + "boolean")); + } + code.unindent(); + code.pr("};"); + code.pr("// Trigger presence projection macros"); + for (var i = 0; i < this.triggerInstances.size(); i++) { + code.pr( + "define " + + this.triggerInstances.get(i).getFullNameWithJoiner("_") + + "_is_present" + + "(t : trigger_t) : boolean = t._" + + (i + 1) + + ";"); + } + + // A boolean tuple indicating whether actions are scheduled by reactions + // at the instant when they are triggered. + code.pr( + String.join( + "\n", + "// A boolean tuple indicating whether actions are scheduled by reactions", + "// at the instant when they are triggered.")); + code.pr("type sched_t = {"); + code.indent(); + if (this.actionInstances.size() > 0) { + for (var i = 0; i < this.actionInstances.size(); i++) { + code.pr( + "boolean" + + ((i == this.actionInstances.size() - 1) ? "" : ",") + + "\t// " + + this.actionInstances.get(i)); + } + } else { + code.pr( + String.join( + "\n", + "// There are no actions.", + "// Insert a dummy boolean to make the model compile.", + "boolean")); + } + code.unindent(); + code.pr("};"); + code.pr("// Projection macros for action schedule flag"); + for (var i = 0; i < this.actionInstances.size(); i++) { + code.pr( + "define " + + this.actionInstances.get(i).getFullNameWithJoiner("_") + + "_scheduled" + + "(d : sched_t) : boolean = d._" + + (i + 1) + + ";"); + } + + // A integer tuple indicating the integer payloads scheduled by reactions + // at the instant when they are triggered. + code.pr( + String.join( + "\n", + "// A integer tuple indicating the integer payloads scheduled by reactions", + "// at the instant when they are triggered.")); + code.pr("type payload_t = {"); + code.indent(); + if (this.actionInstances.size() > 0) { + for (var i = 0; i < this.actionInstances.size(); i++) { + code.pr( + "integer" + + ((i == this.actionInstances.size() - 1) ? "" : ",") + + "\t// " + + this.actionInstances.get(i)); + } + } else { + code.pr( + String.join( + "\n", + "// There are no actions.", + "// Insert a dummy integer to make the model compile.", + "integer")); + } + code.unindent(); + code.pr("};"); + code.pr("// Projection macros for scheduled payloads"); + for (var i = 0; i < this.actionInstances.size(); i++) { + code.pr( + "define " + + this.actionInstances.get(i).getFullNameWithJoiner("_") + + "_scheduled_payload" + + "(payload : payload_t) : integer = payload._" + + (i + 1) + + ";"); + } + } + + /** Axioms for reactor semantics */ + protected void generateReactorSemantics() { + code.pr( + String.join( + "\n", + "/*********************", + " * Reactor Semantics *", + " *********************/", + "")); + + // Non-federated "happened-before" + code.pr( + String.join( + "\n", + "// Non-federated \"happened-before\"", + "define hb(e1, e2 : event_t) : boolean", + "= tag_earlier(e1._2, e2._2)")); + if (!this.logicalTimeBased) { + code.indent(); + // Get happen-before relation between two reactions. + code.pr("|| (tag_same(e1._2, e2._2) && ( false"); + // Iterate over reactions based on upstream/downstream relations. + for (var upstreamRuntime : this.reactionInstances) { + var downstreamReactions = upstreamRuntime.getReaction().dependentReactions(); + for (var downstream : downstreamReactions) { + // If the downstream reaction and the upstream + // reaction are in the same reactor, skip, since + // they will be accounted for in the for loop below. + if (downstream.getParent().equals(upstreamRuntime.getReaction().getParent())) continue; + for (var downstreamRuntime : downstream.getRuntimeInstances()) { + code.pr( + "|| (" + + upstreamRuntime.getReaction().getFullNameWithJoiner("_") + + "(e1._1)" + + " && " + + downstreamRuntime.getReaction().getFullNameWithJoiner("_") + + "(e2._1)" + + ")"); + } + } + } + // Iterate over reactions based on priorities. + for (var reactor : this.reactorInstances) { + for (int i = 0; i < reactor.reactions.size(); i++) { + for (int j = i + 1; j < reactor.reactions.size(); j++) { + code.pr( + "|| (" + + reactor.reactions.get(i).getFullNameWithJoiner("_") + + "(e1._1)" + + " && " + + reactor.reactions.get(j).getFullNameWithJoiner("_") + + "(e2._1)" + + ")"); + } + } + } + code.unindent(); + code.pr("))"); + } + code.pr(";"); + + code.pr( + String.join( + "\n", + "/** transition relation **/", + "// transition relation constrains future states", + "// based on previous states.", + "", + "// Events are ordered by \"happened-before\" relation.", + "axiom(finite_forall (i : integer) in indices :: (i >= START && i <= END_TRACE) ==>" + + " (finite_forall (j : integer) in indices ::", + " (j >= START && j <= END_TRACE) ==> (hb(elem(i), elem(j)) ==> i < j)));", + "", + "// Tags should be non-negative.", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE)", + " ==> pi1(g(i)) >= 0);", + "", + "// Microsteps should be non-negative.", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE)", + " ==> pi2(g(i)) >= 0);", + "", + "// Begin the frame at the start time specified.", + "define start_frame(i : step_t) : boolean =", + " (tag_same(g(i), {start_time, 0}) || tag_later(g(i), {start_time, 0}));", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE)", + " ==> start_frame(i));", + "", + "// NULL events should appear in the suffix, except for START.", + "axiom(finite_forall (j : integer) in indices :: (j > START && j <= END_TRACE) ==> (", + " !isNULL(j)) ==> ", + " (finite_forall (i : integer) in indices :: (i > START && i < j) ==>" + + " (!isNULL(i))));", + "")); + + //// Axioms for the event-based semantics + if (!this.logicalTimeBased) { + code.pr("//// Axioms for the event-based semantics"); + + // the same event can only trigger once in a logical instant + code.pr( + String.join( + "\n", + "// the same event can only trigger once in a logical instant", + "axiom(finite_forall (i : integer) in indices :: (i >= START && i <= END_TRACE) ==>" + + " (finite_forall (j : integer) in indices ::", + " (j >= START && j <= END_TRACE) ==> ((rxn(i) == rxn(j) && i != j)", + " ==> !tag_same(g(i), g(j)))));", + "")); + + // Only one reaction gets triggered at a time. + ArrayList reactionsStatus = new ArrayList<>(); + for (int i = 0; i < this.reactionInstances.size(); i++) reactionsStatus.add("false"); + code.pr( + String.join( + "\n", + "// Only one reaction gets triggered at a time.", + "axiom(finite_forall (i : integer) in indices :: (i >= START && i <= END_TRACE) ==>" + + " (", + " isNULL(i)")); + code.indent(); + for (int i = 0; i < this.reactionInstances.size(); i++) { + String[] li = reactionsStatus.toArray(String[]::new); + li[i] = "true"; + code.pr("|| rxn(i) == " + "{" + String.join(", ", li) + "}"); + } + code.unindent(); + code.pr("));"); + } + } + + /** Axioms for all triggers */ + protected void generateTriggersAndReactions() { + generateConnectionAxioms(); + generateActionAxioms(); + generateTimerAxioms(); + generateReactionTriggerAxioms(); + } + + /** Generate axiomatic semantics for connections */ + protected void generateConnectionAxioms() { + code.pr(String.join("\n", "/***************", " * Connections *", " ***************/")); + // FIXME: Support banks and multiports. Figure out how to work with ranges. + // Iterate over all the ports. Generate an axiom for each connection + // (i.e. a pair of input-output ports). + // A "range" holds the connection information. + // See connectPortInstances() in ReactorInstance.java for more details. + for (var port : this.portInstances) { + for (SendRange range : port.getDependentPorts()) { + PortInstance source = range.instance; + Connection connection = range.connection; + List> destinations = range.destinations; + + // Extract delay value + long delay = 0; + if (connection.getDelay() != null) { + // Somehow delay is an Expression, + // which makes it hard to convert to nanoseconds. + Expression delayExpr = connection.getDelay(); + if (delayExpr instanceof Time) { + long interval = ((Time) delayExpr).getInterval(); + String unit = ((Time) delayExpr).getUnit(); + TimeValue timeValue = new TimeValue(interval, TimeUnit.fromName(unit)); + delay = timeValue.toNanoSeconds(); + } + } + + for (var portRange : destinations) { + var destination = portRange.instance; + + // We have extracted the source, destination, and connection AST node. + // Now we are ready to generate an axiom for this triple. + code.pr( + "// " + + source.getFullNameWithJoiner("_") + + " " + + (connection.isPhysical() ? "~>" : "->") + + " " + + destination.getFullNameWithJoiner("_")); + code.pr( + String.join( + "\n", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END) ==> (", + "// If " + + source.getFullNameWithJoiner("_") + + " is present, then " + + destination.getFullNameWithJoiner("_") + + " will be present.", + "// with the same value after some fixed delay of " + delay + " nanoseconds.", + "(" + source.getFullNameWithJoiner("_") + "_is_present" + "(t(i)) ==> ((", + " finite_exists (j : integer) in indices :: j > i && j <= END_TRACE", + " && " + destination.getFullNameWithJoiner("_") + "_is_present" + "(t(j))", + " && " + + destination.getFullNameWithJoiner("_") + + "(s(j)) == " + + source.getFullNameWithJoiner("_") + + "(s(i))", + connection.isPhysical() ? "" : "&& g(j) == tag_delay(g(i), " + delay + ")", + ")", + ")) // Closes (" + + source.getFullNameWithJoiner("_") + + "_is_present" + + "(t(i)) ==> ((.", + //// Separator + "// If " + + destination.getFullNameWithJoiner("_") + + " is present, there exists an " + + source.getFullNameWithJoiner("_") + + " in prior steps.", + "// This additional term establishes a one-to-one relationship between two ports'" + + " signals.", + "&& (" + destination.getFullNameWithJoiner("_") + "_is_present" + "(t(i)) ==> (", + " finite_exists (j : integer) in indices :: j >= START && j < i", + " && " + source.getFullNameWithJoiner("_") + "_is_present" + "(t(j))", + " && " + + source.getFullNameWithJoiner("_") + + "(s(j)) == " + + destination.getFullNameWithJoiner("_") + + "(s(i))", + connection.isPhysical() ? "" : " && g(i) == tag_delay(g(j), " + delay + ")", + ")) // Closes the one-to-one relationship.", + "));")); + + // If destination is not present, then its value resets to 0. + code.pr( + String.join( + "\n", + "// If " + + destination.getFullNameWithJoiner("_") + + " is not present, then its value resets to 0.", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE &&" + + " !isNULL(i)) ==> (", + " (!" + + destination.getFullNameWithJoiner("_") + + "_is_present" + + "(t(i)) ==> (", + " " + destination.getFullNameWithJoiner("_") + "(s(i)) == 0", + " ))", + "));")); + } + } + } + } + + /** Generate axiomatic semantics for actions */ + protected void generateActionAxioms() { + if (this.actionInstances.size() > 0) { + code.pr(String.join("\n", "/***********", " * Actions *", " ***********/")); + for (var action : this.actionInstances) { + Set dependsOnReactions = action.getDependsOnReactions(); + String comment = + "If " + + action.getFullNameWithJoiner("_") + + " is present, these reactions could schedule it: "; + String triggerStr = ""; + for (var reaction : dependsOnReactions) { + comment += reaction.getFullNameWithJoiner("_") + ", "; + triggerStr += + String.join( + "\n", + "// " + reaction.getFullNameWithJoiner("_"), + // OR because only any present trigger can trigger the reaction. + "|| (" + action.getFullNameWithJoiner("_") + "_is_present" + "(t(i)) ==> (", + " finite_exists (j : integer) in indices :: j >= START && j < i", + " && " + reaction.getFullNameWithJoiner("_") + "(rxn(j))", + " && g(i) == tag_schedule(g(j), " + action.getMinDelay().toNanoSeconds() + ")", + " && " + action.getFullNameWithJoiner("_") + "_scheduled" + "(d(j))", + " && " + + action.getFullNameWithJoiner("_") + + "(s(i))" + + " == " + + action.getFullNameWithJoiner("_") + + "_scheduled_payload" + + "(pl(j))", + "))"); + } + + // After populating the string segments, + // print the generated code string. + code.pr( + String.join( + "\n", + "// " + comment, + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE) ==>" + + " ( false", + triggerStr, + "));")); + + // If the action is not present, then its value resets to 0. + code.pr( + String.join( + "\n", + "// If " + + action.getFullNameWithJoiner("_") + + " is not present, then its value resets to 0.", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE &&" + + " !isNULL(i)) ==> (", + " (!" + action.getFullNameWithJoiner("_") + "_is_present" + "(t(i)) ==> (", + " " + action.getFullNameWithJoiner("_") + "(s(i)) == 0", + " ))", + "));")); + } + } + } + + /** Generate axiomatic semantics for timers */ + protected void generateTimerAxioms() { + if (this.timerInstances.size() > 0) { + code.pr(String.join("\n", "/**********", " * Timers *", " **********/")); + + for (var timer : this.timerInstances) { + long offset = timer.getOffset().toNanoSeconds(); + long period = timer.getPeriod().toNanoSeconds(); + + code.pr("//// Axioms for " + timer.getFullName()); + + // An initial firing at {offset, 0} + code.pr( + String.join( + "\n", + "// " + timer.getFullName() + ": an initial firing at (" + offset + ", 0)", + "axiom(", + " ((pi1(g(END)) >= " + offset + ") ==> (", + " finite_exists (j : integer) in indices :: (j > START && j <= END)", + " && " + timer.getFullNameWithJoiner("_") + "_is_present(t(j))", + " && tag_same(g(j), {" + offset + ", 0})", + " ))", + " && ((pi1(g(END)) < " + offset + ") ==> (", + " finite_forall (i : integer) in indices :: (i > START && i <= END)", + " ==> (!isNULL(i))", + " ))", + ");")); + + // Schedule subsequent firings. + code.pr( + String.join( + "\n", + "// " + + timer.getFullName() + + ": schedule subsequent firings every " + + period + + " ns", + "axiom(", + " finite_forall (i : integer) in indices :: (i >= START && i <= END) ==> (", + " " + timer.getFullNameWithJoiner("_") + "_is_present(t(i)) ==> (", + " (", + " finite_exists (j : integer) in indices :: (j >= START && j > i)", + " && " + timer.getFullNameWithJoiner("_") + "_is_present(t(j))", + " && (g(j) == tag_schedule(g(i), " + period + "))", + " )", + " )", + " )", + ");")); + + // All firings must be evenly spaced out. + code.pr( + String.join( + "\n", + "// " + timer.getFullName() + ": all firings must be evenly spaced out.", + "axiom(", + " finite_forall (i : integer) in indices :: (i >= START && i <= END) ==> (", + " " + timer.getFullNameWithJoiner("_") + "_is_present(t(i)) ==> (", + " // Timestamp must be offset + n * period.", + " (", + " exists (n : integer) :: (", + " n >= 0 &&", + " pi1(g(i)) == " + offset + " + n * " + period, + " )", + " )", + " // Microstep must be 0.", + " && (pi2(g(i)) == 0)", + " )", + " )", + ");")); + } + } + } + + /** Axioms for encoding how reactions are triggered. */ + protected void generateReactionTriggerAxioms() { + code.pr( + String.join( + "\n", + "/********************************", + " * Reactions and Their Triggers *", + " ********************************/")); + // Iterate over all reactions, generate conditions for them + // to be triggered. + outerLoop: + for (ReactionInstance.Runtime reaction : this.reactionInstances) { + String str = + String.join( + "\n", + "// " + + reaction.getReaction().getFullNameWithJoiner("_") + + " is invoked when any of it triggers are present.", + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END_TRACE) ==>" + + " ((", + " false"); + + // Iterate over the triggers of the reaction. + for (TriggerInstance trigger : reaction.getReaction().triggers) { + String triggerPresentStr = ""; + + if (trigger.isStartup()) { + // FIXME: Treat startup as a variable. + // Handle startup. + code.pr( + String.join( + "\n", + "// If startup is within frame (and all variables have default values),", + "// " + reaction.getReaction().getFullNameWithJoiner("_") + " must be invoked.", + "axiom(", + " ((start_time == 0) ==> (", + " finite_exists (i : integer) in indices :: i > START && i <= END", + " && " + + reaction.getReaction().getFullNameWithJoiner("_") + + "(rxn(i))" + + " && tag_same(g(i), zero())", + " && !(", + " finite_exists (j : integer) in indices :: j > START && j <= END", + " && " + + reaction.getReaction().getFullNameWithJoiner("_") + + "(rxn(j))", + " && j != i", + " )", + " ))", + ");")); + continue outerLoop; + } else if (trigger.isShutdown()) { + // FIXME: For a future version. + System.out.println("Not implemented!"); + } else { + // If the trigger is a port/action/timer. + triggerPresentStr = trigger.getFullNameWithJoiner("_") + "_is_present" + "(t(i))"; + } + + // Check if the trigger triggers other reactions. + // If so, we need to assert in the axioms that + // the other reactions are excluded (not invoked), + // to preserve the interleaving semantics. + String exclusion = ""; + for (var instance : trigger.getDependentReactions()) { + for (var runtime : ((ReactionInstance) instance).getRuntimeInstances()) { + if (runtime == reaction) continue; // Skip the current reaction. + exclusion += " && !" + runtime.getReaction().getFullNameWithJoiner("_") + "(rxn(i))"; + } + } + + str += "\n|| (" + triggerPresentStr + exclusion + ")"; + } + + // If any of the above trigger is present, then trigger the reaction. + str += "\n) <==> (" + reaction.getReaction().getFullNameWithJoiner("_") + "(rxn(i))" + ")));"; + code.pr(str); + } + } + + /** Macros for initial conditions */ + protected void generateInitialConditions() { + code.pr( + String.join( + "\n", + "/*********************", + " * Initial Condition *", + " *********************/", + "define initial_condition() : boolean", + "= start_time == 0", + " && isNULL(0)", + " && g(0) == {0, 0}")); + code.indent(); + for (var v : this.stateVariables) { + code.pr("&& " + v.getFullNameWithJoiner("_") + "(s(0))" + " == " + "0"); + } + for (var t : this.triggerInstances) { + code.pr("&& " + t.getFullNameWithJoiner("_") + "(s(0))" + " == " + "0"); + } + for (var t : this.triggerInstances) { + code.pr("&& !" + t.getFullNameWithJoiner("_") + "_is_present" + "(t(0))"); + } + for (var d : this.actionInstances) { + code.pr("&& !" + d.getFullNameWithJoiner("_") + "_scheduled" + "(d(0))"); + } + code.unindent(); + code.pr(";\n"); + } + + /** Lift reaction bodies into Uclid axioms. */ + protected void generateReactionAxioms() { + code.pr(String.join("\n", "/*************", " * Reactions *", " *************/")); + + for (ReactionInstance.Runtime reaction : this.reactionInstances) { + String body = reaction.getReaction().getDefinition().getCode().getBody(); + + // Generate a parse tree. + CLexer lexer = new CLexer(CharStreams.fromString(body)); + CommonTokenStream tokens = new CommonTokenStream(lexer); + CParser parser = new CParser(tokens); + BlockItemListContext parseTree = parser.blockItemList(); + + // Build an AST. + BuildAstParseTreeVisitor buildAstVisitor = new BuildAstParseTreeVisitor(messageReporter); + CAst.AstNode ast = buildAstVisitor.visitBlockItemList(parseTree); + + // VariablePrecedenceVisitor + VariablePrecedenceVisitor precVisitor = new VariablePrecedenceVisitor(); + precVisitor.visit(ast); + + // Convert the AST to If Normal Form (INF). + IfNormalFormAstVisitor infVisitor = new IfNormalFormAstVisitor(); + infVisitor.visit(ast, new ArrayList()); + CAst.StatementSequenceNode inf = infVisitor.INF; + + // For the variables that are USED inside this reaction, extract the conditions + // for setting them, and take the negation of their conjunction + // to get the condition for maintaining their values. + List unusedStates = new ArrayList<>(this.stateVariables); + List unusedOutputs = new ArrayList<>(this.outputInstances); + List unusedActions = new ArrayList<>(this.actionInstances); + HashMap> defaultBehaviorConditions = new HashMap<>(); + for (CAst.AstNode node : inf.children) { + CAst.IfBlockNode ifBlockNode = (CAst.IfBlockNode) node; + // Under the INF form, a C statement is + // the THEN branch of an IF block. + CAst.AstNode stmt = ((CAst.IfBodyNode) ifBlockNode.right).left; + NamedInstance instance = null; + // Match stmt with different cases + if ((stmt instanceof CAst.AssignmentNode + && ((CAst.AssignmentNode) stmt).left instanceof CAst.StateVarNode)) { + CAst.StateVarNode n = (CAst.StateVarNode) ((CAst.AssignmentNode) stmt).left; + instance = + reaction.getReaction().getParent().states.stream() + .filter(s -> s.getName().equals(n.name)) + .findFirst() + .get(); + unusedStates.remove(instance); + } else if (stmt instanceof CAst.SetPortNode) { + CAst.SetPortNode n = (CAst.SetPortNode) stmt; + String name = ((CAst.VariableNode) n.left).name; + instance = + reaction.getReaction().getParent().outputs.stream() + .filter(s -> s.getName().equals(name)) + .findFirst() + .get(); + unusedOutputs.remove(instance); + } else if (stmt instanceof CAst.ScheduleActionNode) { + CAst.ScheduleActionNode n = (CAst.ScheduleActionNode) stmt; + String name = ((CAst.VariableNode) n.children.get(0)).name; + instance = + reaction.getReaction().getParent().actions.stream() + .filter(s -> s.getName().equals(name)) + .findFirst() + .get(); + unusedActions.remove(instance); + } else if (stmt instanceof CAst.ScheduleActionIntNode) { + CAst.ScheduleActionIntNode n = (CAst.ScheduleActionIntNode) stmt; + String name = ((CAst.VariableNode) n.children.get(0)).name; + instance = + reaction.getReaction().getParent().actions.stream() + .filter(s -> s.getName().equals(name)) + .findFirst() + .get(); + unusedStates.remove(instance); + unusedActions.remove(instance); + } else continue; + // Create a new entry in the list if there isn't one yet. + if (defaultBehaviorConditions.get(instance) == null) { + defaultBehaviorConditions.put(instance, new ArrayList()); + } + defaultBehaviorConditions.get(instance).add(ifBlockNode.left); + // System.out.println("DEBUG: Added a reset condition: " + ifBlockNode.left); + } + + // Generate Uclid axiom for the C AST. + CToUclidVisitor c2uVisitor = new CToUclidVisitor(this, reaction); + String axiom = c2uVisitor.visit(inf); + code.pr( + String.join( + "\n", + "// Reaction body of " + reaction, + "axiom(finite_forall (i : integer) in indices :: (i > START && i <= END) ==> (", + " (" + reaction.getReaction().getFullNameWithJoiner("_") + "(rxn(i))" + ")", + " ==> " + "(" + "(" + axiom + ")", + "&& " + "( " + "true")); + for (NamedInstance key : defaultBehaviorConditions.keySet()) { + CAst.AstNode disjunction = AstUtils.takeDisjunction(defaultBehaviorConditions.get(key)); + CAst.LogicalNotNode notNode = new CAst.LogicalNotNode(); + notNode.child = disjunction; + String resetCondition = c2uVisitor.visit(notNode); + + // Check for invalid reset conditions. + // If found, stop the execution. + // FIXME: A more systematic check is needed + // to ensure that the generated Uclid file + // is valid. + if (resetCondition.contains("null")) { + throw new IllegalStateException("Null detected in a reset condition. Stop."); + } + + code.pr("// Unused state variables and ports are reset by default."); + code.pr("&& " + "(" + "(" + resetCondition + ")" + " ==> " + "("); + if (key instanceof StateVariableInstance) { + StateVariableInstance n = (StateVariableInstance) key; + code.pr( + n.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + "i" + + ")" + + ")" + + " == " + + n.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + "i" + + "-1" + + ")" + + ")"); + } else if (key instanceof PortInstance) { + PortInstance n = (PortInstance) key; + code.pr( + "(" + + " true" + // Reset value + + "\n&& " + + n.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + "i" + + ")" + + ")" + + " == " + + "0" // Default value + // Reset presence + + "\n&& " + + n.getFullNameWithJoiner("_") + + "_is_present" + + "(" + + "t" + + "(" + + "i" + + ")" + + ")" + + " == " + + "false" // default presence + + ")"); + } else if (key instanceof ActionInstance) { + ActionInstance n = (ActionInstance) key; + code.pr( + n.getFullNameWithJoiner("_") + + "_scheduled" + + "(" + + "d" + + "(" + + "i" + + ")" + + ")" + + " == " + + "false"); + } else { + throw new AssertionError("unreachable"); + } + code.pr("))"); + } + + // For state variables and ports that are NOT used in this reaction, + // their values stay the same by default. + code.pr("// By default, the value of the variables used in this reaction stay the same."); + if (this.logicalTimeBased) { + // If all other reactions that can modify the SAME state variable + // are not triggered, then the state variable stay the same. + // + // FIXME: What if two reactions modifying the same state variable + // are triggered at the same time? + // How to use axioms to model reaction priority? + // The main difficulty of logical time based semantics is composing + // the effect of simultaneous reactions. + // + // A path way to implement it in the future: + // 1. For each variable, port, and action, determine a list of + // reactions that can modify/schedule it. + // 2. Reaction axioms should be generated wrt each reactor. + // For example, assuming a reactor with two input ports, + // each triggering a distinct reaction. The axioms will need + // to handle four cases: i. reaction 1 gets triggered and 2 + // does not; ii. reaction 2 gets triggered and 1 does not; + // iii. both reactions get triggered; iv. none of them get + // triggered. Since it is hard to specify in an independent way, + // due to reaction priorities, + // what happens when two reactions (modifying the same state var.) + // get triggered simultaneously, some combinatorial blowup will + // be incurred. In this example, four axioms (instead of two), + // each handling one case, seems needed. The good news is that + // axioms across reactors may be specified independently. + // For example, if there is another reactor of the same class, + // Only four more axioms need to be added (in total 2^2 + 2^2), + // instead of 16 axioms (2^4). + } else { + for (StateVariableInstance s : unusedStates) { + code.pr("&& (true ==> ("); + code.pr( + s.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + "i" + + ")" + + ")" + + " == " + + s.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + "i" + + "-1" + + ")" + + ")"); + code.pr("))"); + } + for (PortInstance p : unusedOutputs) { + code.pr("&& (true ==> ("); + code.pr( + "(" + + " true" + // Reset value + + "\n&& " + + p.getFullNameWithJoiner("_") + + "(" + + "s" + + "(" + + "i" + + ")" + + ")" + + " == " + + "0" // Default value + // Reset presence + + "\n&& " + + p.getFullNameWithJoiner("_") + + "_is_present" + + "(" + + "t" + + "(" + + "i" + + ")" + + ")" + + " == " + + false // default presence + + ")"); + code.pr("))"); + } + for (ActionInstance a : unusedActions) { + code.pr("&& (true ==> ("); + code.pr( + a.getFullNameWithJoiner("_") + + "_scheduled" + + "(" + + "d" + + "(" + + "i" + + ")" + + ")" + + " == " + + "false"); + code.pr("))"); + } + code.pr("))));"); + } + } + } + + protected void generateProperty() { + code.pr(String.join("\n", "/************", " * Property *", " ************/")); + + code.pr("// The FOL property translated from user-defined MTL property:"); + code.pr("// " + this.spec); + code.pr("define p(i : step_t) : boolean ="); + code.indent(); + code.pr(this.FOLSpec + ";"); + code.unindent(); + + if (this.tactic == Tactic.BMC) { + code.pr( + String.join( + "\n", + "// BMC", + "property " + "bmc_" + this.name + " : " + "initial_condition() ==> p(0);")); + } else { + code.pr( + String.join( + "\n", + "// Induction: initiation step", + "property " + "initiation_" + this.name + " : " + "initial_condition() ==> p(0);", + "// Induction: consecution step", + "property " + "consecution_" + this.name + " : " + "p(0) ==> p(1);")); + } + } + + /** Uclid5 control block */ + protected void generateControlBlock() { + code.pr( + String.join( + "\n", + "control {", + " v = bmc(0);", + " check;", + " print_results;", + " v.print_cex_json;", + "}")); + } + + //////////////////////////////////////////////////////////// + //// Private methods + + private void setupDirectories() { + // Make sure the target directory exists. + Path modelGenDir = context.getFileConfig().getModelGenPath(); + this.outputDir = Paths.get(modelGenDir.toString()); + try { + Files.createDirectories(outputDir); + } catch (IOException e) { + throw new RuntimeException(e); + } + System.out.println("The models will be located in: " + outputDir); + } + + /** Populate the data structures. */ + private void populateDataStructures() { + // Populate lists of reactor/reaction instances, + // state variables, actions, ports, and timers. + populateLists(this.main); + + // Join actions, ports, and timers into a list of triggers. + this.triggerInstances = new ArrayList(this.actionInstances); + this.triggerInstances.addAll(portInstances); + this.triggerInstances.addAll(timerInstances); + + // Join state variables and triggers + this.namedInstances = new ArrayList(this.stateVariables); + namedInstances.addAll(this.triggerInstances); + } + + private void populateLists(ReactorInstance reactor) { + // Reactor and reaction instances + this.reactorInstances.add(reactor); + for (var reaction : reactor.reactions) { + this.reactionInstances.addAll(reaction.getRuntimeInstances()); + } + + // State variables, actions, ports, timers. + for (var state : reactor.states) { + this.stateVariables.add(state); + } + for (var action : reactor.actions) { + this.actionInstances.add(action); + } + for (var port : reactor.inputs) { + this.inputInstances.add(port); + this.portInstances.add(port); + } + for (var port : reactor.outputs) { + this.outputInstances.add(port); + this.portInstances.add(port); + } + for (var timer : reactor.timers) { + this.timerInstances.add(timer); + } + + // Recursion + for (var child : reactor.children) { + populateLists(child); + } + } + + /** + * Compute a completeness threadhold for each property by simulating a worst-case execution by + * traversing the reactor instance graph and building a state space diagram. + */ + private void computeCT() { + + StateSpaceExplorer explorer = new StateSpaceExplorer(this.main); + explorer.explore( + new Tag(this.horizon, 0, false), true // findLoop + ); + StateSpaceDiagram diagram = explorer.diagram; + diagram.display(); + + // Generate a dot file. + try { + CodeBuilder dot = diagram.generateDot(); + Path file = this.outputDir.resolve(this.tactic + "_" + this.name + ".dot"); + String filename = file.toString(); + dot.writeToFile(filename); + } catch (IOException e) { + throw new RuntimeException(e); + } + + //// Compute CT + if (!explorer.loopFound) { + if (this.logicalTimeBased) this.CT = diagram.nodeCount(); + else { + // FIXME: This could be much more efficient with + // a linkedlist implementation. We can go straight + // to the next node. + StateSpaceNode node = diagram.head; + this.CT = diagram.head.getReactionsInvoked().size(); + while (node != diagram.tail) { + node = diagram.getDownstreamNode(node); + this.CT += node.getReactionsInvoked().size(); + } + } + } + // Over-approximate CT by estimating the number of loop iterations required. + else { + // Subtract the non-periodic logical time + // interval from the total horizon. + long horizonRemained = Math.subtractExact(this.horizon, diagram.loopNode.getTag().timestamp); + + // Check how many loop iteration is required + // to check the remaining horizon. + int loopIterations = 0; + if (diagram.loopPeriod == 0 && horizonRemained != 0) + throw new RuntimeException( + "ERROR: Zeno behavior detected while the horizon is non-zero. The program has no" + + " finite CT."); + else if (diagram.loopPeriod == 0 && horizonRemained == 0) { + // Handle this edge case. + throw new RuntimeException("Unhandled case: both the horizon and period are 0!"); + } else { + loopIterations = (int) Math.ceil((double) horizonRemained / diagram.loopPeriod); + } + + if (this.logicalTimeBased) { + /* + CT = steps required for the non-periodic part + + steps required for the periodic part + + this.CT = (diagram.loopNode.index + 1) + + (diagram.tail.index - diagram.loopNode.index + 1) * loopIterations; + + An overflow-safe version of the line above + */ + int t0 = Math.addExact(diagram.loopNode.getIndex(), 1); + int t1 = Math.subtractExact(diagram.tail.getIndex(), diagram.loopNode.getIndex()); + int t2 = Math.addExact(t1, 1); + int t3 = Math.multiplyExact(t2, loopIterations); + this.CT = Math.addExact(t0, t3); + + } else { + // Get the number of events before the loop starts. + // This stops right before the loopNode is encountered. + StateSpaceNode node = diagram.head; + int numReactionInvocationsBeforeLoop = 0; + while (node != diagram.loopNode) { + numReactionInvocationsBeforeLoop += node.getReactionsInvoked().size(); + node = diagram.getDownstreamNode(node); + } + // Account for the loop node in numReactionInvocationsBeforeLoop. + numReactionInvocationsBeforeLoop += node.getReactionsInvoked().size(); + + // Count the events from the loop node until + // loop node is reached again. + int numReactionInvocationsInsideLoop = 0; + do { + node = diagram.getDownstreamNode(node); + numReactionInvocationsInsideLoop += node.getReactionsInvoked().size(); + } while (node != diagram.loopNode); + + /* + CT = steps required for the non-periodic part + + steps required for the periodic part + + this.CT = numReactionInvocationsBeforeLoop + + numReactionInvocationsInsideLoop * loopIterations; + + An overflow-safe version of the line above + */ + // System.out.println("DEBUG: numReactionInvocationsBeforeLoop: " + + // numReactionInvocationsBeforeLoop); + // System.out.println("DEBUG: numReactionInvocationsInsideLoop: " + + // numReactionInvocationsInsideLoop); + // System.out.println("DEBUG: loopIterations: " + loopIterations); + int t0 = Math.multiplyExact(numReactionInvocationsInsideLoop, loopIterations); + this.CT = Math.addExact(numReactionInvocationsBeforeLoop, t0); + } + } + } + + /** Process an MTL property. */ + private void processMTLSpec() { + MTLLexer lexer = new MTLLexer(CharStreams.fromString(this.spec)); + CommonTokenStream tokens = new CommonTokenStream(lexer); + MTLParser parser = new MTLParser(tokens); + MtlContext mtlCtx = parser.mtl(); + MTLVisitor visitor = new MTLVisitor(this.tactic); + + // The visitor transpiles the MTL into a Uclid axiom. + this.FOLSpec = visitor.visitMtl(mtlCtx, "i", 0, "0", 0); + this.horizon = visitor.getHorizon(); + } + + ///////////////////////////////////////////////// + //// Functions from generatorBase + + @Override + public Target getTarget() { + return Target.C; // Works with a C subset. + } + + @Override + public TargetTypes getTargetTypes() { + throw new UnsupportedOperationException( + "This method is not applicable for this generator since Uclid5 is not an LF target."); + } +} diff --git a/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java b/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java new file mode 100644 index 0000000000..b2fe3ecc71 --- /dev/null +++ b/core/src/main/java/org/lflang/analyses/uclid/UclidRunner.java @@ -0,0 +1,236 @@ +package org.lflang.analyses.uclid; + +import java.io.IOException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import org.json.JSONArray; +import org.json.JSONException; +import org.json.JSONObject; +import org.lflang.analyses.statespace.StateInfo; +import org.lflang.analyses.statespace.Tag; +import org.lflang.generator.GeneratorCommandFactory; +import org.lflang.util.LFCommand; + +/** (EXPERIMENTAL) Runner for Uclid5 models. */ +public class UclidRunner { + + /** A list of paths to the generated files */ + List filePaths; + + /** The directory where the generated files are placed */ + public Path outputDir; + + /** A factory for compiler commands. */ + GeneratorCommandFactory commandFactory; + + /** A UclidGenerator instance */ + UclidGenerator generator; + + // Constructor + public UclidRunner(UclidGenerator generator) { + this.generator = generator; + this.commandFactory = + new GeneratorCommandFactory( + generator.context.getErrorReporter(), generator.context.getFileConfig()); + } + + /** Parse information from an SMT model for a step in the trace. */ + public StateInfo parseStateInfo(String smtStr) { + StateInfo info = new StateInfo(); + + // Check for any let bindings. + Pattern p = + Pattern.compile( + "\\(let \\(\\((a!\\d+) \\(_tuple_\\d+ ((.)+?)\\)\\)\\)(\\\\n" + + "|\\s)+\\(_tuple_\\d+ ((.|\\n" + + ")+)\\)"); + HashMap symbolTable = new HashMap<>(); + Matcher m = p.matcher(smtStr.strip()); + String itemized = ""; + if (m.find()) { + // FIXME: Handle multiple let bindings. + String symbol = m.group(1).strip(); + String value = m.group(2).strip(); + symbolTable.put(symbol, value); + itemized = m.group(5).strip(); + } else { + // Remove the outer tuple layer. + p = Pattern.compile("\\(_tuple_\\d+((.|\\n)*)\\)"); + m = p.matcher(smtStr.strip()); + m.find(); + itemized = m.group(1).strip(); + } + + // Process each sub-tuple by matching (_tuple_n ...) + // or matching a!n, where n is an integer. + p = Pattern.compile("(a!\\d+)|\\(_tuple_\\d+((\\s|\\\\n|\\d|\\(- \\d+\\)|true|false)+)\\)"); + m = p.matcher(itemized); + + // Reactions + m.find(); + String reactionsStr = ""; + // Found a let binding. + if (m.group(1) != null) { + reactionsStr = symbolTable.get(m.group(1)).strip(); + } + // The rest falls into group 2. + else { + reactionsStr = m.group(2).strip(); + } + String[] reactions = reactionsStr.split("\\s+"); + // Iterating over generator lists avoids accounting for + // the single dummy Uclid variable inserted earlier. + for (int i = 0; i < generator.reactionInstances.size(); i++) { + if (reactions[i].equals("true")) + info.reactions.add(generator.reactionInstances.get(i).getReaction().getFullName()); + } + + // Time tag + m.find(); + String tagStr = ""; + // Found a let binding. + if (m.group(1) != null) tagStr = symbolTable.get(m.group(1)).strip(); + // The rest falls into group 2. + else tagStr = m.group(2).strip(); + String[] tag = tagStr.split("\\s+"); + info.tag = new Tag(Long.parseLong(tag[0]), Long.parseLong(tag[1]), false); + + // Variables + // Currently all integers. + // Negative numbers could appear. + m.find(); + String variablesStr = ""; + // Found a let binding. + if (m.group(1) != null) variablesStr = symbolTable.get(m.group(1)).strip(); + // The rest falls into group 2. + else variablesStr = m.group(2).strip(); + String[] variables = variablesStr.replaceAll("\\(-\\s(.*?)\\)", "-$1").split("\\s+"); + for (int i = 0; i < generator.namedInstances.size(); i++) { + info.variables.put(generator.namedInstances.get(i).getFullName(), variables[i]); + } + + // Triggers + m.find(); + String triggersStr = ""; + // Found a let binding. + if (m.group(1) != null) triggersStr = symbolTable.get(m.group(1)).strip(); + // The rest falls into group 2. + else triggersStr = m.group(2).strip(); + String[] triggers = triggersStr.split("\\s+"); + for (int i = 0; i < generator.triggerInstances.size(); i++) { + info.triggers.put(generator.triggerInstances.get(i).getFullName(), triggers[i]); + } + + // Actions scheduled + m.find(); + String scheduledStr = ""; + // Found a let binding. + if (m.group(1) != null) scheduledStr = symbolTable.get(m.group(1)).strip(); + // The rest falls into group 2. + else scheduledStr = m.group(2).strip(); + String[] scheduled = scheduledStr.split("\\s+"); + for (int i = 0; i < generator.actionInstances.size(); i++) { + info.scheduled.put(generator.actionInstances.get(i).getFullName(), scheduled[i]); + } + + // Scheduled payloads + // Currently all integers. + // Negative numbers could appear. + m.find(); + String payloadsStr = ""; + // Found a let binding. + if (m.group(1) != null) payloadsStr = symbolTable.get(m.group(1)).strip(); + // The rest falls into group 2. + else payloadsStr = m.group(2).strip(); + String[] payloads = payloadsStr.replaceAll("\\(-\\s(.*?)\\)", "-$1").split("\\s+"); + for (int i = 0; i < generator.actionInstances.size(); i++) { + info.payloads.put(generator.actionInstances.get(i).getFullName(), payloads[i]); + } + + return info; + } + + /** + * Run all the generated Uclid models, report outputs, and generate counterexample trace diagrams. + */ + public void run() { + for (Path path : generator.generatedFiles) { + // Execute uclid for each property. + LFCommand command = + commandFactory.createCommand( + "uclid", + List.of( + path.toString(), + // Any counterexample will be in .json + "--json-cex", + path.toString()), + generator.outputDir); + command.run(); + + String output = command.getOutput().toString(); + boolean valid = !output.contains("FAILED"); + if (valid) { + System.out.println("Valid!"); + } else { + System.out.println("Not valid!"); + try { + // Read from the JSON counterexample (cex). + String cexJSONStr = + Files.readString(Paths.get(path.toString() + ".json"), StandardCharsets.UTF_8); + JSONObject cexJSON = new JSONObject(cexJSONStr); + + //// Extract the counterexample trace from JSON. + // Get the first key "property_*" + Iterator keys = cexJSON.keys(); + String firstKey = keys.next(); + JSONObject propertyObj = cexJSON.getJSONObject(firstKey); + + // Get Uclid trace. + JSONArray uclidTrace = propertyObj.getJSONArray("trace"); + + // Get the first step of the Uclid trace. + JSONObject uclidTraceStepOne = uclidTrace.getJSONObject(0); + + // Get the actual trace defined in the verification model. + JSONObject trace = uclidTraceStepOne.getJSONArray("trace").getJSONObject(0); + + String stepStr = ""; + for (int i = 0; i <= generator.CT; i++) { + try { + stepStr = trace.getString(String.valueOf(i)); + } catch (JSONException e) { + stepStr = trace.getString("-"); + } + System.out.println("============ Step " + i + " ============"); + StateInfo info = parseStateInfo(stepStr); + info.display(); + } + } catch (IOException e) { + System.out.println("ERROR: Not able to read from " + path.toString()); + } + } + + // If "expect" is set, check if the result matches it. + // If not, exit with error code 1. + String expect = generator.expectations.get(path); + if (expect != null) { + boolean expectValid = Boolean.parseBoolean(expect); + if (expectValid != valid) { + System.out.println( + "ERROR: The expected result does not match the actual result. Expected: " + + expectValid + + ", Result: " + + valid); + System.exit(1); + } + } + } + } +} diff --git a/core/src/main/java/org/lflang/ast/ASTUtils.java b/core/src/main/java/org/lflang/ast/ASTUtils.java index 3484dbfe18..93c689b810 100644 --- a/core/src/main/java/org/lflang/ast/ASTUtils.java +++ b/core/src/main/java/org/lflang/ast/ASTUtils.java @@ -58,7 +58,9 @@ import org.eclipse.xtext.xbase.lib.IteratorExtensions; import org.eclipse.xtext.xbase.lib.StringExtensions; import org.lflang.InferredType; +import org.lflang.MessageReporter; import org.lflang.Target; +import org.lflang.TargetConfig; import org.lflang.TimeUnit; import org.lflang.TimeValue; import org.lflang.generator.CodeMap; @@ -146,6 +148,22 @@ public static List getAllReactors(Resource resource) { .collect(Collectors.toList()); } + /** + * Get the main reactor defined in the given resource. + * + * @param resource the resource to extract reactors from + * @return An iterable over all reactors found in the resource + */ + public static Reactor getMainReactor(Resource resource) { + return StreamSupport.stream( + IteratorExtensions.toIterable(resource.getAllContents()).spliterator(), false) + .filter(Reactor.class::isInstance) + .map(Reactor.class::cast) + .filter(it -> it.isMain()) + .findFirst() + .get(); + } + /** * Find connections in the given resource that would be conflicting writes if they were not * located in mutually exclusive modes. @@ -570,6 +588,40 @@ public static List collectElements( return result; } + /** + * If a main or federated reactor has been declared, create a ReactorInstance for this top level. + * This will also assign levels to reactions, then, if the program is federated, perform an AST + * transformation to disconnect connections between federates. + */ + public static ReactorInstance createMainReactorInstance( + Instantiation mainDef, + List reactors, + MessageReporter messageReporter, + TargetConfig targetConfig) { + if (mainDef != null) { + // Recursively build instances. + ReactorInstance main = + new ReactorInstance(toDefinition(mainDef.getReactorClass()), messageReporter, reactors); + var reactionInstanceGraph = main.assignLevels(); + if (reactionInstanceGraph.nodeCount() > 0) { + messageReporter + .nowhere() + .error("Main reactor has causality cycles. Skipping code generation."); + return null; + } + // Inform the run-time of the breadth/parallelism of the reaction graph + var breadth = reactionInstanceGraph.getBreadth(); + if (breadth == 0) { + messageReporter.nowhere().warning("The program has no reactions"); + } else { + targetConfig.compileDefinitions.put( + "LF_REACTION_GRAPH_BREADTH", String.valueOf(reactionInstanceGraph.getBreadth())); + } + return main; + } + return null; + } + /** * Adds the elements into the given list at a location matching to their textual position. * diff --git a/core/src/main/java/org/lflang/generator/GeneratorBase.java b/core/src/main/java/org/lflang/generator/GeneratorBase.java index 4109ec96c9..dde30f5580 100644 --- a/core/src/main/java/org/lflang/generator/GeneratorBase.java +++ b/core/src/main/java/org/lflang/generator/GeneratorBase.java @@ -26,7 +26,6 @@ import com.google.common.base.Objects; import com.google.common.collect.Iterables; -import java.io.IOException; import java.nio.file.Path; import java.nio.file.Paths; import java.util.ArrayList; @@ -145,12 +144,6 @@ public Instantiation getMainDef() { /** Indicates whether the current Lingua Franca program contains model reactors. */ public boolean hasModalReactors = false; - /** - * Indicates whether the program has any deadlines and thus needs to propagate deadlines through - * the reaction instance graph - */ - public boolean hasDeadlines = false; - /** Indicates whether the program has any watchdogs. This is used to check for support. */ public boolean hasWatchdogs = false; @@ -180,24 +173,6 @@ protected void registerTransformation(AstTransformation transformation) { // ////////////////////////////////////////// // // Code generation functions to override for a concrete code generator. - /** - * If there is a main or federated reactor, then create a synthetic Instantiation for that - * top-level reactor and set the field mainDef to refer to it. - */ - private void createMainInstantiation() { - // Find the main reactor and create an AST node for its instantiation. - Iterable nodes = - IteratorExtensions.toIterable(context.getFileConfig().resource.getAllContents()); - for (Reactor reactor : Iterables.filter(nodes, Reactor.class)) { - if (reactor.isMain()) { - // Creating a definition for the main reactor because there isn't one. - this.mainDef = LfFactory.eINSTANCE.createInstantiation(); - this.mainDef.setName(reactor.getName()); - this.mainDef.setReactorClass(reactor); - } - } - } - /** * Generate code from the Lingua Franca model contained by the specified resource. * @@ -212,10 +187,6 @@ private void createMainInstantiation() { */ public void doGenerate(Resource resource, LFGeneratorContext context) { - // FIXME: the signature can be reduced to only take context. - // The constructor also need not take a file config because this is tied to the context as well. - cleanIfNeeded(context); - printInfo(context.getMode()); // Clear any IDE markers that may have been created by a previous build. @@ -296,13 +267,20 @@ public void doGenerate(Resource resource, LFGeneratorContext context) { additionalPostProcessingForModes(); } - /** Check if a clean was requested from the standalone compiler and perform the clean step. */ - protected void cleanIfNeeded(LFGeneratorContext context) { - if (context.getArgs().containsKey("clean")) { - try { - context.getFileConfig().doClean(); - } catch (IOException e) { - System.err.println("WARNING: IO Error during clean"); + /** + * If there is a main or federated reactor, then create a synthetic Instantiation for that + * top-level reactor and set the field mainDef to refer to it. + */ + protected void createMainInstantiation() { + // Find the main reactor and create an AST node for its instantiation. + Iterable nodes = + IteratorExtensions.toIterable(context.getFileConfig().resource.getAllContents()); + for (Reactor reactor : Iterables.filter(nodes, Reactor.class)) { + if (reactor.isMain()) { + // Creating a definition for the main reactor because there isn't one. + this.mainDef = LfFactory.eINSTANCE.createInstantiation(); + this.mainDef.setName(reactor.getName()); + this.mainDef.setReactorClass(reactor); } } } diff --git a/core/src/main/java/org/lflang/generator/LFGenerator.java b/core/src/main/java/org/lflang/generator/LFGenerator.java index 261a615b91..410051f835 100644 --- a/core/src/main/java/org/lflang/generator/LFGenerator.java +++ b/core/src/main/java/org/lflang/generator/LFGenerator.java @@ -2,17 +2,23 @@ import com.google.inject.Inject; import com.google.inject.Injector; +import java.io.BufferedReader; import java.io.IOException; +import java.io.InputStreamReader; import java.nio.file.Path; import java.util.Arrays; +import java.util.List; +import java.util.stream.Collectors; import org.eclipse.emf.ecore.resource.Resource; import org.eclipse.xtext.generator.AbstractGenerator; import org.eclipse.xtext.generator.IFileSystemAccess2; import org.eclipse.xtext.generator.IGeneratorContext; import org.eclipse.xtext.util.RuntimeIOException; +import org.lflang.AttributeUtils; import org.lflang.FileConfig; import org.lflang.MessageReporter; import org.lflang.Target; +import org.lflang.analyses.uclid.UclidGenerator; import org.lflang.ast.ASTUtils; import org.lflang.federated.generator.FedASTUtils; import org.lflang.federated.generator.FedFileConfig; @@ -27,6 +33,8 @@ import org.lflang.generator.rust.RustGenerator; import org.lflang.generator.ts.TSFileConfig; import org.lflang.generator.ts.TSGenerator; +import org.lflang.lf.Attribute; +import org.lflang.lf.Reactor; import org.lflang.scoping.LFGlobalScopeProvider; /** Generates code from your model files on save. */ @@ -109,6 +117,12 @@ public void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorCont } else { + // If "-c" or "--clean" is specified, delete any existing generated directories. + cleanIfNeeded(lfContext); + + // If @property annotations are used, run the LF verifier. + runVerifierIfPropertiesDetected(resource, lfContext); + final GeneratorBase generator = createGenerator(lfContext); if (generator != null) { @@ -126,4 +140,92 @@ public void doGenerate(Resource resource, IFileSystemAccess2 fsa, IGeneratorCont public boolean errorsOccurred() { return generatorErrorsOccurred; } + + /** Check if a clean was requested from the standalone compiler and perform the clean step. */ + protected void cleanIfNeeded(LFGeneratorContext context) { + if (context.getArgs().containsKey("clean")) { + try { + context.getFileConfig().doClean(); + } catch (IOException e) { + System.err.println("WARNING: IO Error during clean"); + } + } + } + + /** + * Check if @property is used. If so, instantiate a UclidGenerator. The verification model needs + * to be generated before the target code since code generation changes LF program (desugar + * connections, etc.). + */ + private void runVerifierIfPropertiesDetected(Resource resource, LFGeneratorContext lfContext) { + Reactor main = ASTUtils.getMainReactor(resource); + final MessageReporter messageReporter = lfContext.getErrorReporter(); + List properties = + AttributeUtils.getAttributes(main).stream() + .filter(attr -> attr.getAttrName().equals("property")) + .collect(Collectors.toList()); + if (properties.size() > 0) { + + // Provide a warning. + messageReporter + .nowhere() + .warning( + "Verification using \"@property\" and \"--verify\" is an experimental feature. Use" + + " with caution."); + + // Generate uclid files. + UclidGenerator uclidGenerator = new UclidGenerator(lfContext, properties); + uclidGenerator.doGenerate(resource, lfContext); + + // Check the generated uclid files. + if (uclidGenerator.targetConfig.verify) { + + // Check if Uclid5 and Z3 are installed. + if (!execInstalled("uclid", "--help", "uclid 0.9.5") + || !execInstalled("z3", "--version", "Z3 version")) { + messageReporter + .nowhere() + .error( + "Fail to check the generated verification models because Uclid5 or Z3 is not" + + " installed."); + } else { + // Run the Uclid tool. + uclidGenerator.runner.run(); + } + + } else { + messageReporter + .nowhere() + .warning( + "The \"verify\" target property is set to false. Skip checking the verification" + + " model. To check the generated verification models, set the \"verify\"" + + " target property to true or pass \"--verify\" to the lfc command"); + } + } + } + + /** + * A helper function for checking if a dependency is installed on the command line. + * + * @param binaryName The name of the binary + * @param arg An argument following the binary name + * @param expectedSubstring An expected substring in the output + * @return + */ + public static boolean execInstalled(String binaryName, String arg, String expectedSubstring) { + ProcessBuilder processBuilder = new ProcessBuilder(binaryName, arg); + try { + Process process = processBuilder.start(); + BufferedReader reader = new BufferedReader(new InputStreamReader(process.getInputStream())); + String line; + while ((line = reader.readLine()) != null) { + if (line.contains(expectedSubstring)) { + return true; + } + } + } catch (IOException e) { + return false; // binary not present + } + return false; + } } diff --git a/core/src/main/java/org/lflang/generator/LFGeneratorContext.java b/core/src/main/java/org/lflang/generator/LFGeneratorContext.java index cc3b41c6c1..4353e3c46e 100644 --- a/core/src/main/java/org/lflang/generator/LFGeneratorContext.java +++ b/core/src/main/java/org/lflang/generator/LFGeneratorContext.java @@ -28,6 +28,7 @@ enum BuildParm { LOGGING("The logging level to use by the generated binary"), LINT("Enable or disable linting of generated code."), NO_COMPILE("Do not invoke target compiler."), + VERIFY("Check the generated verification model."), OUTPUT_PATH("Specify the root output directory."), PRINT_STATISTICS("Instruct the runtime to collect and print statistics."), QUIET("Suppress output of the target compiler and other commands"), diff --git a/core/src/main/java/org/lflang/generator/NamedInstance.java b/core/src/main/java/org/lflang/generator/NamedInstance.java index 3455bcdf40..51b55f026f 100644 --- a/core/src/main/java/org/lflang/generator/NamedInstance.java +++ b/core/src/main/java/org/lflang/generator/NamedInstance.java @@ -97,6 +97,28 @@ public String getFullName() { return getFullNameWithJoiner("."); } + /** + * Return a string of the form "a.b.c", where "." is replaced by the specified joiner, "c" is the + * name of this instance, "b" is the name of its container, and "a" is the name of its container, + * stopping at the container in main. + * + * @return A string representing this instance. + */ + public String getFullNameWithJoiner(String joiner) { + // This is not cached because _uniqueID is cached. + if (parent == null) { + return this.getName(); + } else if (getMode(true) != null) { + return parent.getFullNameWithJoiner(joiner) + + joiner + + getMode(true).getName() + + joiner + + this.getName(); + } else { + return parent.getFullNameWithJoiner(joiner) + joiner + this.getName(); + } + } + /** * Return the name of this instance as given in its definition. Note that this is unique only * relative to other instances with the same parent. @@ -274,31 +296,6 @@ public ModeInstance getMode(boolean direct) { */ int width = 1; - ////////////////////////////////////////////////////// - //// Protected methods. - - /** - * Return a string of the form "a.b.c", where "." is replaced by the specified joiner, "c" is the - * name of this instance, "b" is the name of its container, and "a" is the name of its container, - * stopping at the container in main. - * - * @return A string representing this instance. - */ - protected String getFullNameWithJoiner(String joiner) { - // This is not cached because _uniqueID is cached. - if (parent == null) { - return this.getName(); - } else if (getMode(true) != null) { - return parent.getFullNameWithJoiner(joiner) - + joiner - + getMode(true).getName() - + joiner - + this.getName(); - } else { - return parent.getFullNameWithJoiner(joiner) + joiner + this.getName(); - } - } - ////////////////////////////////////////////////////// //// Protected fields. diff --git a/core/src/main/java/org/lflang/generator/ReactionInstance.java b/core/src/main/java/org/lflang/generator/ReactionInstance.java index a1e35ffb19..41958d921a 100644 --- a/core/src/main/java/org/lflang/generator/ReactionInstance.java +++ b/core/src/main/java/org/lflang/generator/ReactionInstance.java @@ -120,7 +120,9 @@ public ReactionInstance( this.sources.add(timerInstance); } } else if (trigger instanceof BuiltinTriggerRef) { - this.triggers.add(parent.getOrCreateBuiltinTrigger((BuiltinTriggerRef) trigger)); + var builtinTriggerInstance = parent.getOrCreateBuiltinTrigger((BuiltinTriggerRef) trigger); + this.triggers.add(builtinTriggerInstance); + builtinTriggerInstance.dependentReactions.add(this); } } // Next handle the ports that this reaction reads. diff --git a/core/src/main/java/org/lflang/generator/ReactorInstance.java b/core/src/main/java/org/lflang/generator/ReactorInstance.java index 0fbab57aaa..fc436bdb27 100644 --- a/core/src/main/java/org/lflang/generator/ReactorInstance.java +++ b/core/src/main/java/org/lflang/generator/ReactorInstance.java @@ -59,6 +59,7 @@ import org.lflang.lf.Reaction; import org.lflang.lf.Reactor; import org.lflang.lf.ReactorDecl; +import org.lflang.lf.StateVar; import org.lflang.lf.Timer; import org.lflang.lf.VarRef; import org.lflang.lf.Variable; @@ -133,7 +134,7 @@ public ReactorInstance(Reactor reactor, ReactorInstance parent, MessageReporter //// Public fields. /** The action instances belonging to this reactor instance. */ - public List actions = new ArrayList<>(); + public final List actions = new ArrayList<>(); /** * The contained reactor instances, in order of declaration. For banks of reactors, this includes @@ -148,6 +149,9 @@ public ReactorInstance(Reactor reactor, ReactorInstance parent, MessageReporter /** The output port instances belonging to this reactor instance. */ public final List outputs = new ArrayList<>(); + /** The state variable instances belonging to this reactor instance. */ + public final List states = new ArrayList<>(); + /** The parameters of this instance. */ public final List parameters = new ArrayList<>(); @@ -856,17 +860,22 @@ public ReactorInstance( this.parameters.add(new ParameterInstance(parameter, this)); } - // Instantiate inputs for this reactor instance + // Instantiate inputs for this reactor instance. for (Input inputDecl : ASTUtils.allInputs(reactorDefinition)) { this.inputs.add(new PortInstance(inputDecl, this, reporter)); } - // Instantiate outputs for this reactor instance + // Instantiate outputs for this reactor instance. for (Output outputDecl : ASTUtils.allOutputs(reactorDefinition)) { this.outputs.add(new PortInstance(outputDecl, this, reporter)); } - // Do not process content (except interface above) if recursive + // Instantiate state variables for this reactor instance. + for (StateVar state : ASTUtils.allStateVars(reactorDefinition)) { + this.states.add(new StateVariableInstance(state, this, reporter)); + } + + // Do not process content (except interface above) if recursive. if (!recursive && (desiredDepth < 0 || this.depth < desiredDepth)) { // Instantiate children for this reactor instance. // While doing this, assign an index offset to each. diff --git a/core/src/main/java/org/lflang/generator/StateVariableInstance.java b/core/src/main/java/org/lflang/generator/StateVariableInstance.java new file mode 100644 index 0000000000..502825d198 --- /dev/null +++ b/core/src/main/java/org/lflang/generator/StateVariableInstance.java @@ -0,0 +1,79 @@ +/** A data structure for a state variable. */ + +/************* + * Copyright (c) 2019-2022, The University of California at Berkeley. + * + * 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. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "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 COPYRIGHT HOLDER OR CONTRIBUTORS 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. + ***************/ +package org.lflang.generator; + +import org.lflang.MessageReporter; +import org.lflang.lf.StateVar; + +/** Representation of a compile-time instance of a state variable. */ +public class StateVariableInstance extends NamedInstance { + + /** + * Create a runtime instance from the specified definition and with the specified parent that + * instantiated it. + * + * @param definition The declaration in the AST. + * @param parent The parent. + */ + public StateVariableInstance(StateVar definition, ReactorInstance parent) { + this(definition, parent, null); + } + + /** + * Create a port instance from the specified definition and with the specified parent that + * instantiated it. + * + * @param definition The declaration in the AST. + * @param parent The parent. + * @param errorReporter An error reporter, or null to throw exceptions. + */ + public StateVariableInstance( + StateVar definition, ReactorInstance parent, MessageReporter errorReporter) { + super(definition, parent); + + if (parent == null) { + throw new NullPointerException("Cannot create a StateVariableInstance with no parent."); + } + } + + ////////////////////////////////////////////////////// + //// Public methods + + /** + * Return the name of this trigger. + * + * @return The name of this trigger. + */ + @Override + public String getName() { + return definition.getName(); + } + + @Override + public String toString() { + return "StateVariableInstance " + getFullName(); + } +} diff --git a/core/src/main/java/org/lflang/generator/c/CGenerator.java b/core/src/main/java/org/lflang/generator/c/CGenerator.java index e3955d63df..f18035c3e0 100644 --- a/core/src/main/java/org/lflang/generator/c/CGenerator.java +++ b/core/src/main/java/org/lflang/generator/c/CGenerator.java @@ -1952,7 +1952,8 @@ protected void setUpGeneralParameters() { "LOG_LEVEL", String.valueOf(targetConfig.logLevel.ordinal())); targetConfig.compileAdditionalSources.addAll(CCoreFilesUtils.getCTargetSrc()); // Create the main reactor instance if there is a main reactor. - createMainReactorInstance(); + this.main = + ASTUtils.createMainReactorInstance(mainDef, reactors, messageReporter, targetConfig); if (hasModalReactors) { // So that each separate compile knows about modal reactors, do this: targetConfig.compileDefinitions.put("MODAL_REACTORS", "TRUE"); @@ -2099,39 +2100,6 @@ public Target getTarget() { //////////////////////////////////////////////////////////// //// Private methods - /** - * If a main or federated reactor has been declared, create a ReactorInstance for this top level. - * This will also assign levels to reactions, then, if the program is federated, perform an AST - * transformation to disconnect connections between federates. - */ - private void createMainReactorInstance() { - if (this.mainDef != null) { - if (this.main == null) { - // Recursively build instances. - this.main = - new ReactorInstance(toDefinition(mainDef.getReactorClass()), messageReporter, reactors); - var reactionInstanceGraph = this.main.assignLevels(); - if (reactionInstanceGraph.nodeCount() > 0) { - messageReporter - .nowhere() - .error("Main reactor has causality cycles. Skipping code generation."); - return; - } - if (hasDeadlines) { - this.main.assignDeadlines(); - } - // Inform the run-time of the breadth/parallelism of the reaction graph - var breadth = reactionInstanceGraph.getBreadth(); - if (breadth == 0) { - messageReporter.nowhere().warning("The program has no reactions"); - } else { - targetConfig.compileDefinitions.put( - "LF_REACTION_GRAPH_BREADTH", String.valueOf(reactionInstanceGraph.getBreadth())); - } - } - } - } - /** * Generate an array of self structs for the reactor and one for each of its children. * diff --git a/core/src/main/java/org/lflang/validation/AttributeSpec.java b/core/src/main/java/org/lflang/validation/AttributeSpec.java index 90e7f9cf6d..6baf4c17a9 100644 --- a/core/src/main/java/org/lflang/validation/AttributeSpec.java +++ b/core/src/main/java/org/lflang/validation/AttributeSpec.java @@ -217,7 +217,17 @@ enum AttrParamType { ATTRIBUTE_SPECS_BY_NAME.put( "enclave", new AttributeSpec(List.of(new AttrParamSpec(EACH_ATTR, AttrParamType.BOOLEAN, true)))); - + // @property(name="", tactic="", spec="") + // SMTL is the safety fragment of Metric Temporal Logic (MTL). + ATTRIBUTE_SPECS_BY_NAME.put( + "property", + new AttributeSpec( + List.of( + new AttrParamSpec("name", AttrParamType.STRING, false), + new AttrParamSpec("tactic", AttrParamType.STRING, false), + new AttrParamSpec("spec", AttrParamType.STRING, false), + new AttrParamSpec("CT", AttrParamType.INT, true), + new AttrParamSpec("expect", AttrParamType.BOOLEAN, true)))); // attributes that are used internally only by the federated code generation ATTRIBUTE_SPECS_BY_NAME.put("_unordered", new AttributeSpec(null)); ATTRIBUTE_SPECS_BY_NAME.put( diff --git a/core/src/testFixtures/java/org/lflang/tests/Configurators.java b/core/src/testFixtures/java/org/lflang/tests/Configurators.java index 4fd80816e1..4191687278 100644 --- a/core/src/testFixtures/java/org/lflang/tests/Configurators.java +++ b/core/src/testFixtures/java/org/lflang/tests/Configurators.java @@ -113,6 +113,7 @@ public static boolean compatibleWithThreadingOff(TestCategory category) { || category == TestCategory.DOCKER_FEDERATED || category == TestCategory.DOCKER || category == TestCategory.ARDUINO + || category == TestCategory.VERIFIER || category == TestCategory.ZEPHYR_UNTHREADED || category == TestCategory.ZEPHYR_THREADED; diff --git a/core/src/testFixtures/java/org/lflang/tests/TestBase.java b/core/src/testFixtures/java/org/lflang/tests/TestBase.java index b1b52b0c2e..92eeba5734 100644 --- a/core/src/testFixtures/java/org/lflang/tests/TestBase.java +++ b/core/src/testFixtures/java/org/lflang/tests/TestBase.java @@ -156,6 +156,7 @@ public static class Message { public static final String DESC_SCHED_SWAPPING = "Running with non-default runtime scheduler "; public static final String DESC_ROS2 = "Running tests using ROS2."; public static final String DESC_MODAL = "Run modal reactor tests."; + public static final String DESC_VERIFIER = "Run verifier tests."; /* Missing dependency messages */ public static final String MISSING_DOCKER = diff --git a/core/src/testFixtures/java/org/lflang/tests/TestRegistry.java b/core/src/testFixtures/java/org/lflang/tests/TestRegistry.java index 53dda29121..27e1d26d3f 100644 --- a/core/src/testFixtures/java/org/lflang/tests/TestRegistry.java +++ b/core/src/testFixtures/java/org/lflang/tests/TestRegistry.java @@ -334,6 +334,7 @@ public enum TestCategory { ARDUINO(false, "", TestLevel.BUILD), ZEPHYR_THREADED(false, "zephyr" + File.separator + "threaded", TestLevel.BUILD), ZEPHYR_UNTHREADED(false, "zephyr" + File.separator + "unthreaded", TestLevel.BUILD), + VERIFIER(false, "verifier", TestLevel.EXECUTION), TARGET(false, "", TestLevel.EXECUTION); /** Whether we should compare coverage against other targets. */ diff --git a/gradle.properties b/gradle.properties index 7dbf2e0d4f..fd082fc31f 100644 --- a/gradle.properties +++ b/gradle.properties @@ -3,11 +3,14 @@ group=org.lflang version=0.4.1-SNAPSHOT [versions] +antlrVersion=4.7.2 fasterxmlVersion=2.12.4 googleJavaFormatVersion=1.15.0 jacocoVersion=0.8.7 +jsonVersion=20200518 jupiterVersion=5.8.2 jUnitPlatformVersion=1.8.2 +klighdVersion=2.3.0.v20230606 kotlinJvmTarget=17 lsp4jVersion=0.21.0 mwe2LaunchVersion=2.14.0 @@ -25,4 +28,3 @@ org.eclipse.lsp4j=lsp4jVersion org.opentest4j=openTest4jVersion org.eclipse.core.resources=resourcesVersion org.junit.jupiter=jupiterVersion - diff --git a/test/C/src/verifier/ADASModel.lf b/test/C/src/verifier/ADASModel.lf new file mode 100644 index 0000000000..41f8e27ace --- /dev/null +++ b/test/C/src/verifier/ADASModel.lf @@ -0,0 +1,93 @@ +target C + +preamble {= + typedef int c_frame_t; + typedef int l_frame_t; +=} + +reactor Camera { + output out: {= c_frame_t =} + state frame: {= c_frame_t =} + timer t(0, 17 msec) // 60 fps + + reaction(t) -> out {= + // Capture a frame. + self->frame = 1; + lf_set(out, self->frame); + =} +} + +reactor LiDAR { + output out: {= l_frame_t =} + state frame: {= l_frame_t =} + timer t(0, 34 msec) // 30 fps + + reaction(t) -> out {= + // Capture a frame. + self->frame = 2; + lf_set(out, self->frame); + =} +} + +reactor Pedal { + output out: int + physical action a + + reaction(a) -> out {= lf_set(out, 1); =} +} + +reactor Brakes { + input inADAS: int + input inPedal: int + state brakesApplied: int = 0 + + reaction(inADAS, inPedal) {= + // Actuate brakes. + self->brakesApplied = 1; + =} deadline(10 msec) {= =} +} + +reactor ADASProcessor { + input in1: {= l_frame_t =} + input in2: {= c_frame_t =} + output out1: int + output out2: int + logical action a(50 msec) + state requestStop: int + + reaction(in1, in2) -> a {= + // ... Detect danger + // and request stop. + lf_schedule(a, 0); + self->requestStop = 1; + =} + + reaction(a) -> out1, out2 {= + if (self->requestStop == 1) + lf_set(out1, 1); + =} deadline(20 msec) {= =} +} + +reactor Dashboard { + input in: int + state received: int + + reaction(in) {= self->received = 1; =} +} + +@property( + name = "responsive", + tactic = "bmc", + spec = "G[0, 10 ms]((ADASModel_l_reaction_0 && (F[0](ADASModel_p_requestStop == 1))) ==> (F[0, 55 ms]( ADASModel_b_brakesApplied == 1 )))", + expect = true) +main reactor ADASModel { + c = new Camera() + l = new LiDAR() + p = new ADASProcessor() + b = new Brakes() + d = new Dashboard() + l.out -> p.in1 // p = new Pedal(); + c.out -> p.in2 + p.out2 -> d.in + p.out1 -> b.inADAS after 5 msec // p.out -> b.inPedal; +} diff --git a/test/C/src/verifier/AircraftDoor.lf b/test/C/src/verifier/AircraftDoor.lf new file mode 100644 index 0000000000..ab6390ffbe --- /dev/null +++ b/test/C/src/verifier/AircraftDoor.lf @@ -0,0 +1,46 @@ +target C + +reactor Controller { + output out: int + + reaction(startup) -> out {= lf_set(out, 1); =} +} + +reactor Vision { + input in: int + output out: int + state ramp: int = 0 + + reaction(in) -> out {= + if (self->ramp == 1) { + lf_set(out, 0); // 0 = Do not open. + } else { + lf_set(out, 1); // 1 = Open. + } + =} +} + +reactor Door { + input in: int + state doorOpen: int + + reaction(in) {= + if (in->value == 1) + self->doorOpen = 1; // Open + else if (in->value == 0) + self->doorOpen = 0; // Closed + =} +} + +@property( + name = "vision_works", + tactic = "bmc", + spec = "((AircraftDoor_vision_ramp == 0) ==> (G[0 sec](AircraftDoor_door_reaction_0 ==> (AircraftDoor_door_doorOpen == 1))))", + expect = true) +main reactor AircraftDoor { + controller = new Controller() + vision = new Vision() + door = new Door() + controller.out -> vision.in + vision.out -> door.in +} diff --git a/test/C/src/verifier/Alarm.lf b/test/C/src/verifier/Alarm.lf new file mode 100644 index 0000000000..6449f8d626 --- /dev/null +++ b/test/C/src/verifier/Alarm.lf @@ -0,0 +1,38 @@ +target C + +reactor Controller { + output out: int + output out2: int + state fault: int + + logical action turnOff(1 sec): int + + @label("Computation") + reaction(startup) -> out, out2, turnOff {= + // ... Operation + self->fault = 1; // Fault occurs + + // Fault handling + if (self->fault == 1) { + lf_schedule(turnOff, 0); // Wrong action value. Should be 1. + lf_set(out, 5); + lf_set(out2, 10); + } + =} + + @label("Stop") + reaction(turnOff) {= + // Trigger the alarm and reset fault. + if (turnOff->value == 1) + self->fault = 0; + =} +} + +@property( + name = "machine_stops_within_1_sec", + tactic = "bmc", + spec = "G[0, 1 sec]((Alarm_c_reaction_0) ==> F(0, 1 sec](Alarm_c_reaction_1)))", + expect = true) +main reactor { + c = new Controller() +} diff --git a/test/C/src/verifier/CoopSchedule.lf b/test/C/src/verifier/CoopSchedule.lf new file mode 100644 index 0000000000..c755ef7559 --- /dev/null +++ b/test/C/src/verifier/CoopSchedule.lf @@ -0,0 +1,36 @@ +target C + +reactor Trigger { + output out: int + timer t(0, 1 usec) + + reaction(t) -> out {= lf_set(out, 1); =} +} + +reactor Task { + input cnt: int + state counter: int = 0 + + reaction(cnt) {= + self->counter += 2; // Should be 1. + =} +} + +@property( + name = "upperbound", + tactic = "bmc", + spec = "G[0, 1 usec]((CoopSchedule_task1_counter + CoopSchedule_task2_counter + CoopSchedule_task3_counter + CoopSchedule_task4_counter + CoopSchedule_task5_counter) < 15)", + expect = false) +main reactor { + trigger = new Trigger() + task1 = new Task() // TODO: Put these reactors in a bank. + task2 = new Task() + task3 = new Task() + task4 = new Task() + task5 = new Task() + trigger.out -> task1.cnt + trigger.out -> task2.cnt + trigger.out -> task3.cnt + trigger.out -> task4.cnt + trigger.out -> task5.cnt +} diff --git a/test/C/src/verifier/Election2.lf b/test/C/src/verifier/Election2.lf new file mode 100644 index 0000000000..a94ac19429 --- /dev/null +++ b/test/C/src/verifier/Election2.lf @@ -0,0 +1,76 @@ +target C + +reactor Node0 { + input in: int + output out: int + state id: int + state elected: int = 0 + + reaction(startup) -> out {= + self->id = 0; + lf_set(out, self->id); + =} + + reaction(in) -> out {= + if (in->value > self->id) { + lf_set(out, in->value); + } else if (in->value == self->id) { + self->elected = 1; + } + =} +} + +reactor Node1 { + input in: int + output out: int + state id: int + state elected: int = 0 + + reaction(startup) -> out {= + self->id = 1; + lf_set(out, self->id); + =} + + reaction(in) -> out {= + if (in->value > self->id) { + lf_set(out, in->value); + } else if (in->value == self->id) { + self->elected = 1; + } + =} +} + +reactor Node2 { + input in: int + output out: int + state id: int + state elected: int = 0 + + reaction(startup) -> out {= + self->id = 2; + lf_set(out, self->id); + =} + + reaction(in) -> out {= + if (in->value > self->id) { + lf_set(out, in->value); + } else if (in->value == self->id) { + self->elected = 1; + } + =} +} + +// This property being checked does not hold. A valid property is F[0, 30 msec]((Election2_i0_elected + Election2_i1_elected + Election2_i2_elected) == 1) +@property( + name = "exactly_one_elected", + tactic = "bmc", + spec = "F[0, 20 msec]((Election2_i0_elected + Election2_i1_elected + Election2_i2_elected) == 1)", + expect = false) +main reactor { + i0 = new Node0() + i1 = new Node1() + i2 = new Node2() + i0.out -> i1.in after 10 msec + i1.out -> i2.in after 10 msec + i2.out -> i0.in after 10 msec +} diff --git a/test/C/src/verifier/PingPongVerifier.lf b/test/C/src/verifier/PingPongVerifier.lf new file mode 100644 index 0000000000..b69f99aa3a --- /dev/null +++ b/test/C/src/verifier/PingPongVerifier.lf @@ -0,0 +1,68 @@ +/** + * Basic benchmark from the Savina benchmark suite that is intended to measure message-passing + * overhead. This is based on https://www.scala-lang.org/old/node/54 See + * https://shamsimam.github.io/papers/2014-agere-savina.pdf. + * + * Ping introduces a microstep delay using a logical action to break the causality loop. + * + * To get a sense, some (informal) results for 1,000,000 ping-pongs on my Mac: + * + * - Unthreaded: 97 msec + * - Threaded: 265 msec + * + * There is no parallelism in this application, so it does not benefit from being being threaded, + * just some additional overhead. + * + * These measurements are total execution time, including startup and shutdown. These are about an + * order of magnitude faster than anything reported in the paper. + */ +target C { + fast: true +} + +reactor Ping { + input receive: int + output send: int + state pingsLeft: int = 10 + logical action serve(1 nsec) + + reaction(startup) -> serve {= + self->pingsLeft = 10; + lf_schedule(serve, 0); + =} + + reaction(serve) -> send {= + lf_set(send, self->pingsLeft); + self->pingsLeft -= 1; + =} + + reaction(receive) -> serve {= + if (self->pingsLeft > 0) { + lf_schedule(serve, 0); + } + =} +} + +reactor Pong { + input receive: int + output send: int + state count: int = 0 + state expected: int = 10 + + reaction(receive) -> send {= + self->count += 1; + lf_set(send, receive->value); + =} +} + +@property( + name = "no_two_consecutive_pings", + tactic = "bmc", + spec = "G[0, 4 nsec](PingPongVerifier_ping_reaction_1 ==> X(!PingPongVerifier_ping_reaction_1))", + expect = false) +main reactor PingPongVerifier { + ping = new Ping() + pong = new Pong() + ping.send -> pong.receive + pong.send -> ping.receive +} diff --git a/test/C/src/verifier/ProcessMsg.lf b/test/C/src/verifier/ProcessMsg.lf new file mode 100644 index 0000000000..ce9a2090d7 --- /dev/null +++ b/test/C/src/verifier/ProcessMsg.lf @@ -0,0 +1,42 @@ +target C + +reactor Task { + input in: int + output out: int + + state messageSent: int + state counter: int = 0 + state panic: int = 0 + + timer t(0, 1 nsec) + + logical action updateMessage + + reaction(startup) {= self->messageSent = 0; =} + + reaction(t) -> out {= lf_set(out, self->messageSent); =} + + reaction(in) -> updateMessage {= + /* Check for invalid message. */ + if (in->value != self->messageSent) { + self->panic = 1; + } + lf_schedule(updateMessage, 0); + self->counter += 1; + =} + + reaction(updateMessage) {= + /* Increment the last word of the 16-byte message. */ + self->messageSent += 1; + =} +} + +@property( + name = "panic_free", + tactic = "bmc", + spec = "G[5 nsec](ProcessMsg_task_panic != 1)", + expect = true) +main reactor { + task = new Task() + task.out -> task.in +} diff --git a/test/C/src/verifier/ProcessSync.lf b/test/C/src/verifier/ProcessSync.lf new file mode 100644 index 0000000000..cc045810ea --- /dev/null +++ b/test/C/src/verifier/ProcessSync.lf @@ -0,0 +1,21 @@ +target C + +reactor Task { + /** Define the counters used in the demo application... */ + state tm_synchronization_processing_counter: int = 0 + timer t(0, 1 nsec) + + reaction(t) {= + /* Increment the counter. */ + self->tm_synchronization_processing_counter += 1; + =} +} + +@property( + name = "correctness", + tactic = "bmc", + spec = "G[2 nsec](ProcessSync_task_tm_synchronization_processing_counter == 3)", + expect = true) +main reactor { + task = new Task() +} diff --git a/test/C/src/verifier/Ring.lf b/test/C/src/verifier/Ring.lf new file mode 100644 index 0000000000..eb289e1f24 --- /dev/null +++ b/test/C/src/verifier/Ring.lf @@ -0,0 +1,50 @@ +/** There seems to be some problem with infinite feedback loops. */ +target C + +reactor Source { + input in: int + output out: int + logical action start(1 nsec) + state received: int + + reaction(startup) -> start {= + self->received = 0; + lf_schedule(start, 0); + =} + + reaction(start) -> out {= lf_set(out, self->received); =} + + /** Uncomment the following to debug feedback loops. */ + // reaction(in) -> start {= + reaction(in) {= + self->received = in->value; + // lf_schedule(start, 0); + =} +} + +reactor Node { + input in: int + output out: int + + reaction(in) -> out {= lf_set(out, in->value + 1); =} +} + +@property( + name = "full_circle", + tactic = "bmc", + spec = "F[0, 10 nsec](Ring_s_reaction_2)", + expect = true) +main reactor { + s = new Source() + n1 = new Node() + n2 = new Node() + n3 = new Node() + n4 = new Node() + n5 = new Node() + s.out -> n1.in after 1 nsec + n1.out -> n2.in after 1 nsec + n2.out -> n3.in after 1 nsec + n3.out -> n4.in after 1 nsec + n4.out -> n5.in after 1 nsec + n5.out -> s.in after 1 nsec +} diff --git a/test/C/src/verifier/SafeSend.lf b/test/C/src/verifier/SafeSend.lf new file mode 100644 index 0000000000..da21ef589f --- /dev/null +++ b/test/C/src/verifier/SafeSend.lf @@ -0,0 +1,57 @@ +/** + * (Original) Description: This example illustrates the "Verify Absence-of-Errors" mode. The server + * expects a tuple `{REQUEST,PID-OF-SENDER}` but the main sends to it an atom instead of its pid, + * then generating an exception when the server tries to send back a response to what he assumes to + * be a pid. + * + * The verification step discovers a *genuine* counter-example. To inspect the error trace run bfc + * on the generated model and look at the trace alongside the dot model of the ACS. + */ +target C + +reactor Client { + input in: int + output out: int + state req: int = 0 + + reaction(startup) -> out {= + // Sends a query + self->req = 1; // 1 is valid. 0 is invalid. + lf_set(out, self->req); + =} + + reaction(in) {= + // Should not be invoked. + self->req = 0; + =} +} + +reactor Server { + input in: int + output out: int + state error: int + logical action err + + reaction(in) -> out, err {= + if (in->value == 0) { + lf_schedule(err, 0); + } + else { + lf_set(out, in->value); + } + =} + + reaction(err) {= self->error = 1; =} // Error handling logic. +} + +@property( + name = "success", + tactic = "bmc", + spec = "(F[0, 1 sec](SafeSend_c_reaction_1))", + expect = true) +main reactor { + c = new Client() + s = new Server() + c.out -> s.in after 1 nsec + s.out -> c.in +} diff --git a/test/C/src/verifier/Thermostat.lf b/test/C/src/verifier/Thermostat.lf new file mode 100644 index 0000000000..0b583d307d --- /dev/null +++ b/test/C/src/verifier/Thermostat.lf @@ -0,0 +1,67 @@ +/** A thermostat model based on Lee & Seshia Chapter 3, Example 3.5. */ +target C + +reactor Environment { + input heatOn: int + output temperature: int + timer t(1 nsec, 10 sec) + state _heatOn: int + state _temperature: int + + reaction(startup) {= self->_temperature = 19; =} + + reaction(t) -> temperature {= + if (self->_heatOn == 0) { + self->_temperature -= 1; + } + else { + self->_temperature += 1; + } + lf_set(temperature, self->_temperature); + =} + + reaction(heatOn) {= self->_heatOn = heatOn->value; =} +} + +reactor _Thermostat { + input temperature: int + output heatOn: int // 0 = OFF, 1 = ON + state _mode: int // 0 = COOLING, 1 = HEATING + logical action changeMode + + reaction(startup) {= self->_mode = 0; =} + + reaction(temperature) -> heatOn, changeMode {= + if (self->_mode == 0) { + if (temperature->value <= 18) { + lf_set(heatOn, 1); + lf_schedule(changeMode, 0); + } + } + else if (self->_mode == 0) { + if (temperature->value >= 22) { + lf_set(heatOn, 0); + lf_schedule(changeMode, 0); + } + } + =} + + reaction(changeMode) {= + if (self->_mode == 0) + self->_mode = 1; + else + self->_mode = 0; + =} +} + +@property( + name = "correctness", + tactic = "bmc", + spec = "G[0, 20 sec](((Thermostat_t_temperature <= 18) ==> F[0](Thermostat_t__mode == 1)) && ((Thermostat_t_temperature >= 22) ==> F[0](Thermostat_t__mode == 0)))", + expect = true) +main reactor { + e = new Environment() + t = new _Thermostat() + e.temperature -> t.temperature + t.heatOn -> e.heatOn +} diff --git a/test/C/src/verifier/TrainDoor.lf b/test/C/src/verifier/TrainDoor.lf new file mode 100644 index 0000000000..d39f473bea --- /dev/null +++ b/test/C/src/verifier/TrainDoor.lf @@ -0,0 +1,38 @@ +target C + +reactor Controller { + output out1: int + output out2: int + + reaction(startup) -> out1, out2 {= + lf_set(out1, 1); + lf_set(out2, 2); + =} +} + +reactor Train { + input in: int + state received: int + + reaction(in) {= self->received = in->value; =} +} + +reactor Door { + input in: int + state received: int + + reaction(in) {= self->received = in->value; =} +} + +@property( + name = "train_does_not_move_until_door_closes", + tactic = "bmc", + spec = "(!TrainDoor_t_reaction_0)U[0, 1 sec](TrainDoor_d_reaction_0)", + expect = false) +main reactor { + c = new Controller() + t = new Train() + d = new Door() + c.out1 -> t.in after 1 sec + c.out2 -> d.in after 1 sec +} diff --git a/test/C/src/verifier/UnsafeSend.lf b/test/C/src/verifier/UnsafeSend.lf new file mode 100644 index 0000000000..73c3585885 --- /dev/null +++ b/test/C/src/verifier/UnsafeSend.lf @@ -0,0 +1,57 @@ +/** + * (Original) Description: This example illustrates the "Verify Absence-of-Errors" mode. The server + * expects a tuple `{REQUEST,PID-OF-SENDER}` but the main sends to it an atom instead of its pid, + * then generating an exception when the server tries to send back a response to what he assumes to + * be a pid. + * + * The verification step discovers a *genuine* counter-example. To inspect the error trace run bfc + * on the generated model and look at the trace alongside the dot model of the ACS. + */ +target C + +reactor Client { + input in: int + output out: int + state req: int = 0 + + reaction(startup) -> out {= + // Sends a query + self->req = 0; // 1 is valid. 0 is invalid. + lf_set(out, self->req); + =} + + reaction(in) {= + // Should not be invoked. + self->req = 0; + =} +} + +reactor Server { + input in: int + output out: int + state error: int + logical action err(1 nsec) + + reaction(in) -> out, err {= + if (in->value == 0) { + lf_schedule(err, 0); + } + else { + lf_set(out, in->value); + } + =} + + reaction(err) {= self->error = 1; =} // Error handling logic. +} + +@property( + name = "success", + tactic = "bmc", + spec = "(F[0, 5 nsec](UnsafeSend_c_reaction_1))", + expect = false) +main reactor { + c = new Client() + s = new Server() + c.out -> s.in after 2 nsec + s.out -> c.in after 2 nsec +}