Get rid of shell

JetBrains-Research · Oct 9, 2024 · a88e54f · a88e54f
1 parent 18828d2
commit a88e54f
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 12 deletions.
diff --git a/verified_cogen/args.py b/verified_cogen/args.py
@@ -12,7 +12,6 @@ class ProgramArgs:
     insert_conditions_mode: str
     bench_type: str
     temperature: int
-    shell: str
     verifier_command: str
     verifier_timeout: int
     prompts_directory: str
@@ -34,7 +33,6 @@ def __init__(self, args):
         self.insert_conditions_mode = args.insert_conditions_mode
         self.bench_type = args.bench_type
         self.temperature = args.temperature
-        self.shell = args.shell
         self.verifier_command = args.verifier_command
         self.verifier_timeout = args.verifier_timeout
         self.prompts_directory = args.prompts_directory
@@ -67,7 +65,6 @@ def get_default_parser():
         default="invariants",
     )
     parser.add_argument("--temperature", help="model temperature", default=0, type=int)
-    parser.add_argument("--shell", help="shell", default=os.getenv("SHELL"))
     parser.add_argument(
         "--verifier-command",
         help="command to run (cmd [file_path]) to verify a file",

diff --git a/verified_cogen/experiments/incremental_run.py b/verified_cogen/experiments/incremental_run.py
@@ -68,7 +68,7 @@ def main():
     assert len(files) > 0, "No files found in the directory"
     files.sort()
 
-    verifier = Verifier(args.shell, args.verifier_command)
+    verifier = Verifier(args.verifier_command)
 
     for file in files:
         llm = LLM(

diff --git a/verified_cogen/experiments/use_houdini.py b/verified_cogen/experiments/use_houdini.py
@@ -1,7 +1,6 @@
 import argparse
 import json
 import logging
-import os
 from typing import Optional, no_type_check
 
 from verified_cogen.llm import LLM
@@ -230,7 +229,7 @@ def main():
     log.info("Collected {} invariants".format(len(invariants)))
     log.debug("Invariants: {}".format(json.dumps(invariants, indent=4)))
 
-    verifier = Verifier(os.environ["SHELL"], args.verifier_command)
+    verifier = Verifier(args.verifier_command)
     result = houdini(args, verifier, prg, invariants)
     if result is not None:
         log.info("Vefication successful")

diff --git a/verified_cogen/main.py b/verified_cogen/main.py
@@ -142,7 +142,7 @@ def main():
         args.input = input("Input file: ").strip()
     log_tries = pathlib.Path(args.log_tries) if args.log_tries is not None else None
 
-    verifier = Verifier(args.shell, args.verifier_command, args.verifier_timeout)
+    verifier = Verifier(args.verifier_command, args.verifier_timeout)
     if args.dir is not None:
         files = sorted(list(pathlib.Path(args.dir).glob(ext_glob(args.filter_by_ext))))
         runner_cls = make_runner_cls(

diff --git a/verified_cogen/tools/verifier.py b/verified_cogen/tools/verifier.py
@@ -8,17 +8,14 @@
 
 
 class Verifier:
-    def __init__(self, shell: str, verifier_cmd: str, timeout: int = 60):
-        self.shell = shell
+    def __init__(self, verifier_cmd: str, timeout: int = 60):
         self.verifier_cmd = verifier_cmd
         self.timeout = timeout
 
     def verify(self, file_path: Path) -> Optional[tuple[bool, str, str]]:
         try:
             res = subprocess.run(
-                '{} -i -l -c "{} "{}""; exit'.format(
-                    self.shell, self.verifier_cmd, file_path
-                ),
+                '{} "{}"'.format(self.verifier_cmd, file_path),
                 capture_output=True,
                 shell=True,
                 timeout=self.timeout,