pyk: added --llvm-hidden-visibility attribute (#4714)

Author: traiansf

pyk/src/pyk/__main__.py

@@ -324,6 +324,7 @@ def exec_kompile(options: KompileCommandOptions) -> None:
         kompile_dict['llvm_kompile_output'] = options.llvm_kompile_output
         kompile_dict['llvm_proof_hint_instrumentation'] = options.llvm_proof_hint_instrumentation
         kompile_dict['llvm_proof_hint_debugging'] = options.llvm_proof_hint_debugging
+        kompile_dict['llvm_hidden_visibility'] = options.llvm_hidden_visibility
     elif len(options.ccopts) > 0:
         raise ValueError(f'Option `-ccopt` requires `--backend llvm`, not: --backend {options.backend.value}')
     elif options.enable_search:
@@ -344,6 +345,10 @@ def exec_kompile(options: KompileCommandOptions) -> None:
         raise ValueError(
             f'Option `--llvm-proof-hint-debugging` requires `--backend llvm`, not: --backend {options.backend.value}'
         )
+    elif options.llvm_hidden_visibility:
+        raise ValueError(
+            f'Option `--llvm-hidden-visibility` requires `--backend llvm`, not: --backend {options.backend.value}'
+        )
 
     try:
         Kompile.from_dict(kompile_dict)(

pyk/src/pyk/cli/args.py

@@ -194,6 +194,7 @@ class KompileOptions(Options):
     llvm_kompile_output: Path | None
     llvm_proof_hint_instrumentation: bool
     llvm_proof_hint_debugging: bool
+    llvm_hidden_visibility: bool
     read_only: bool
     o0: bool
     o1: bool
@@ -220,6 +221,7 @@ def default() -> dict[str, Any]:
             'llvm_kompile_output': None,
             'llvm_proof_hint_instrumentation': False,
             'llvm_proof_hint_debugging': False,
+            'llvm_hidden_visibility': False,
             'read_only': False,
             'o0': False,
             'o1': False,
@@ -479,6 +481,13 @@ def kompile_args(self) -> ArgumentParser:
             action='store_true',
             help='Enable additional proof hint debugging information in LLVM backend kompilation.',
         )
+        args.add_argument(
+            '--llvm-hidden-visibility',
+            dest='llvm_hidden_visibility',
+            default=None,
+            action='store_true',
+            help='Whether to make all symbols hidden by default in LLVM backend kompilation.',
+        )
 
         args.add_argument(
             '--no-exc-wrap',

pyk/src/pyk/ktool/kompile.py

@@ -428,6 +428,7 @@ class LLVMKompile(Kompile):
     enable_llvm_debug: bool
     llvm_proof_hint_instrumentation: bool
     llvm_proof_hint_debugging: bool
+    llvm_hidden_visibility: bool
     llvm_mutable_bytes: bool
     iterated_threshold: Fraction | None
     heuristic: str | None
@@ -445,6 +446,7 @@ def __init__(
         enable_llvm_debug: bool = False,
         llvm_proof_hint_instrumentation: bool = False,
         llvm_proof_hint_debugging: bool = False,
+        llvm_hidden_visibility: bool = False,
         llvm_mutable_bytes: bool = False,
         iterated_threshold: Fraction | None = None,
         heuristic: str | None = None,
@@ -468,6 +470,7 @@ def __init__(
         object.__setattr__(self, 'enable_llvm_debug', enable_llvm_debug)
         object.__setattr__(self, 'llvm_proof_hint_instrumentation', llvm_proof_hint_instrumentation)
         object.__setattr__(self, 'llvm_proof_hint_debugging', llvm_proof_hint_debugging)
+        object.__setattr__(self, 'llvm_hidden_visibility', llvm_hidden_visibility)
         object.__setattr__(self, 'llvm_mutable_bytes', llvm_mutable_bytes)
         object.__setattr__(self, 'iterated_threshold', iterated_threshold)
         object.__setattr__(self, 'heuristic', heuristic)
@@ -507,6 +510,9 @@ def args(self) -> list[str]:
         if self.llvm_proof_hint_debugging:
             args += ['--llvm-proof-hint-debugging']
 
+        if self.llvm_hidden_visibility:
+            args += ['--llvm-hidden-visibility']
+
         if self.llvm_mutable_bytes:
             args += ['--llvm-mutable-bytes']