Build llvm library in foundry-kompile by default

runtimeverification · Aug 4, 2023 · a8b0126 · a8b0126
1 parent 745feef
commit a8b0126
Show file tree

Hide file tree

Showing 3 changed files with 31 additions and 3 deletions.
diff --git a/.github/workflows/master-push.yml b/.github/workflows/master-push.yml
@@ -104,7 +104,7 @@ jobs:
           docker cp ./tests/foundry ${container_name}:/home/user/foundry
           docker exec -u user ${container_name} /bin/bash -c "sudo chown user:user -R /home/user/foundry"
           docker exec -u user ${container_name} /bin/bash -c "forge build --root foundry"
-          docker exec -u user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose --with-llvm-library"
+          docker exec -u user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose"
           docker exec -u user ${container_name} /bin/bash -c "kevm foundry-prove --foundry-project-root foundry --verbose --test AssertTest.test_assert_true_branch"
           docker exec -u user ${container_name} /bin/bash -c "kevm foundry-show --foundry-project-root foundry --verbose AssertTest.test_assert_true_branch"
           docker exec -u user ${container_name} /bin/bash -c "kevm foundry-list --foundry-project-root foundry --verbose"

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -271,7 +271,7 @@ jobs:
           docker cp ./tests/foundry ${container_name}:/home/user/foundry
           docker exec -u user ${container_name} /bin/bash -c "sudo chown user:user -R /home/user/foundry"
           docker exec -u user ${container_name} /bin/bash -c "forge build --root foundry"
-          docker exec -u user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose --with-llvm-library"
+          docker exec -u user ${container_name} /bin/bash -c "kevm foundry-kompile --foundry-project-root foundry --verbose"
           docker exec -u user ${container_name} /bin/bash -c "kevm foundry-prove --foundry-project-root foundry --verbose --test AssertTest.test_assert_true_branch"
           docker exec -u user ${container_name} /bin/bash -c "kevm foundry-show --foundry-project-root foundry --verbose AssertTest.test_assert_true_branch"
           docker exec -u user ${container_name} /bin/bash -c "kevm foundry-list --foundry-project-root foundry --verbose"

diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -799,6 +799,7 @@ def parse(s: str) -> list[T]:
         'kompile',
         help='Kompile KEVM specification.',
         parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args],
+        conflict_handler='resolve',
     )
     kevm_kompile_args.add_argument('main_file', type=file_path, help='Path to file with main module.')
     kevm_kompile_args.add_argument(
@@ -807,6 +808,19 @@ def parse(s: str) -> list[T]:
     kevm_kompile_args.add_argument(
         '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.'
     )
+    kevm_kompile_args.add_argument(
+        '--with-llvm-library',
+        dest='llvm_library',
+        default=False,
+        action='store_true',
+        help='Do not generate a dynamic llvm library during kompile.',
+    )
+    kevm_kompile_args.add_argument(
+        '--no-llvm-library',
+        dest='llvm_library',
+        action='store_false',
+        help='Make kompile generate a dynamic llvm library.',
+    )
 
     prove_args = command_parser.add_parser(
         'prove',
@@ -921,6 +935,7 @@ def parse(s: str) -> list[T]:
             kevm_cli_args.kompile_args,
             kevm_cli_args.foundry_args,
         ],
+        conflict_handler='resolve',
     )
     foundry_kompile.add_argument(
         '--regen',
@@ -936,6 +951,19 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Rekompile foundry.k even if kompiled definition already exists.',
     )
+    foundry_kompile.add_argument(
+        '--with-llvm-library',
+        dest='llvm_library',
+        default=True,
+        action='store_true',
+        help='Make kompile generate a dynamic llvm library.',
+    )
+    foundry_kompile.add_argument(
+        '--no-llvm-library',
+        dest='llvm_library',
+        action='store_false',
+        help='Do not generate a dynamic llvm library during kompile.',
+    )
 
     foundry_prove_args = command_parser.add_parser(
         'foundry-prove',
@@ -979,7 +1007,7 @@ def parse(s: str) -> list[T]:
         dest='bmc_depth',
         default=None,
         type=int,
-        help='Max depth of loop unrolling during bounded model checking (default: 3).',
+        help='Max depth of loop unrolling during bounded model checking.',
     )
     foundry_prove_args.add_argument(
         '--use-booster',