Support removing implementations

verified_cogen/args.py

@@ -24,6 +24,7 @@ class ProgramArgs:
     log_tries: Optional[str]
     output_logging: bool
     remove_conditions: bool
+    remove_implementations: bool
 
     @no_type_check
     def __init__(self, args):
@@ -45,6 +46,7 @@ def __init__(self, args):
         self.log_tries = args.log_tries
         self.output_logging = args.output_logging
         self.remove_conditions = args.remove_conditions
+        self.remove_implementations = args.remove_implementations
 
 
 def get_default_parser():
@@ -105,6 +107,12 @@ def get_default_parser():
         default=False,
         action="store_true",
     )
+    parser.add_argument(
+        "--remove-implementations",
+        help="Remove implementations from the program",
+        default=False,
+        action="store_true",
+    )
     return parser
 
 

verified_cogen/experiments/incremental_run.py

@@ -40,6 +40,9 @@ def main():
     all_removed = [AnnotationType.INVARIANTS, AnnotationType.ASSERTS]
     if args.remove_conditions:
         all_removed += [AnnotationType.PRE_CONDITIONS, AnnotationType.POST_CONDITIONS]
+    if args.remove_implementations:
+        all_removed += [AnnotationType.IMPLS]
+
     register_basic_languages(with_removed=all_removed)
 
     mode = Mode(args.insert_conditions_mode)

verified_cogen/main.py

@@ -126,6 +126,8 @@ def main():
     all_removed = [AnnotationType.INVARIANTS, AnnotationType.ASSERTS]
     if args.remove_conditions:
         all_removed += [AnnotationType.PRE_CONDITIONS, AnnotationType.POST_CONDITIONS]
+    if args.remove_implementations:
+        all_removed += [AnnotationType.IMPLS]
     register_basic_languages(with_removed=all_removed)
     mode = Mode(args.insert_conditions_mode)
     if mode == Mode.REGEX:

verified_cogen/runners/languages/dafny.py

@@ -18,6 +18,7 @@ def __init__(self, remove_annotations: list[AnnotationType]):  # type: ignore
             AnnotationType.ASSERTS: r" *// assert-start.*?// assert-end\n",
             AnnotationType.PRE_CONDITIONS: r" *// pre-conditions-start.*?// pre-conditions-end\n",
             AnnotationType.POST_CONDITIONS: r" *// post-conditions-start.*?// post-conditions-end\n",
+            AnnotationType.IMPLS: r" *// impl-start.*?// impl-end\n",
         }
         super().__init__(
             re.compile(
@@ -41,3 +42,18 @@ def _validators_from(
             ", ".join(f"ret{i}" for i in range(len(returns.split(",")))),
         )
         return result
+
+    def separate_validator_errors(self, errors: str) -> tuple[str, str]:
+        lines = errors.split("\n")
+        lines = [
+            line for line in lines if "Dafny program verifier finished" not in line
+        ]
+        line_with_ret0 = next(
+            (i for i, line in enumerate(lines) if "ret0" in line), None
+        )
+        if line_with_ret0 is None:
+            return "\n".join(lines), ""
+        else:
+            non_verifier_errors = "\n".join(lines[: line_with_ret0 - 2]).strip()
+            verifier_errors = "\n".join(lines[line_with_ret0 - 2 :]).strip()
+            return non_verifier_errors, verifier_errors

verified_cogen/runners/languages/language.py

@@ -8,6 +8,7 @@ class AnnotationType(Enum):
     ASSERTS = "asserts"
     PRE_CONDITIONS = "pre-conditions"
     POST_CONDITIONS = "post-conditions"
+    IMPLS = "impls"
 
 
 class Language:
@@ -22,6 +23,9 @@ def generate_validators(self, code: str) -> str: ...
     @abstractmethod
     def remove_conditions(self, code: str) -> str: ...
 
+    @abstractmethod
+    def separate_validator_errors(self, errors: str) -> tuple[str, str]: ...
+
 
 class GenericLanguage(Language):
     method_regex: Pattern[str]

verified_cogen/runners/languages/nagini.py

@@ -33,3 +33,8 @@ def __init__(self, remove_annotations: list[AnnotationType]):  # type: ignore
             "# assert-line",
             "#",
         )
+
+    def separate_validator_errors(self, errors: str) -> tuple[str, str]:
+        raise NotImplementedError(
+            "Separating validator errors is not implemented for Verus yet"
+        )

verified_cogen/runners/languages/verus.py

@@ -36,3 +36,8 @@ def __init__(self, remove_annotations: list[AnnotationType]):  # type: ignore
     def generate_validators(self, code: str) -> str:
         result = super().generate_validators(code)
         return "verus!{{\n{}}}".format(result)
+
+    def separate_validator_errors(self, errors: str) -> tuple[str, str]:
+        raise NotImplementedError(
+            "Separating validator errors is not implemented for Verus yet"
+        )

verified_cogen/runners/validating.py

@@ -5,7 +5,6 @@
 from verified_cogen.runners import Runner
 from verified_cogen.runners.languages.language import Language
 from verified_cogen.tools.modes import Mode
-from verified_cogen.tools.dafny_separate import dafny_separate
 
 
 class ValidatingRunner(Runner):
@@ -64,7 +63,7 @@ def ask_for_timeout(self) -> str:
     def ask_for_fixed(self, err: str) -> str:
         assert self.starting_prg is not None
 
-        result, validator = dafny_separate(err)
+        result, validator = self.language.separate_validator_errors(err)
         if validator:
             self.summarizer_llm.add_user_prompt(
                 "Here are the errors you need to summarize:\n" + validator,