Uclid5-based LF Verifier

.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' }}

.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

.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

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)))
+}

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."

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);
     }

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

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;
   }
 }

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);
+  }
+}