Merge pull request #48 from NethermindEth/ElijahVlasov/missining-iden…

…tifier-fix Pretty printing of ```MissingIdentiferError```
NethermindEth · Jan 23, 2023 · 30a8c35 · 30a8c35
2 parents db1e3a4 + 4b062b2
commit 30a8c35
Show file tree

Hide file tree

Showing 3 changed files with 52 additions and 48 deletions.
diff --git a/pyproject.toml b/pyproject.toml
@@ -18,7 +18,7 @@ skip_gitignore = true
 
 [tool.poetry]
 name = "horus-compile"
-version = "0.0.6.5"
+version = "0.0.6.6"
 authors = ["Nethermind <[email protected]>"]
 description = "Use formally verified annotations in your Cairo code"
 classifiers = [

diff --git a/src/horus/__init__.py b/src/horus/__init__.py
@@ -1 +1 @@
-__version__ = "0.0.6.5"
+__version__ = "0.0.6.6"
diff --git a/src/horus/compiler/preprocessor.py b/src/horus/compiler/preprocessor.py
@@ -19,6 +19,7 @@
     LabelDefinition,
     StructDefinition,
 )
+from starkware.cairo.lang.compiler.identifier_manager import MissingIdentifierError
 from starkware.cairo.lang.compiler.identifier_utils import get_struct_definition
 from starkware.cairo.lang.compiler.scoped_name import ScopedName
 from starkware.starknet.compiler.starknet_preprocessor import (
@@ -319,56 +320,59 @@ def append_check(
             self.specifications[self.current_scope] = current_annotations
 
         for parsed_check in self.current_checks:
-            if (
-                isinstance(parsed_check, CodeElementCheck)
-                and parsed_check.check_kind == INVARIANT
-            ):
-                if not isinstance(code_elem, CodeElementLabel):
-                    raise PreprocessorError(
-                        "@invariant annotation must be placed before a label",
-                        code_elem.location,
-                    )
-            elif isinstance(parsed_check, CodeElementCheck):
-                if not (
-                    isinstance(code_elem, CodeElementFunction)
-                    and code_elem.element_type == "func"
+            try:
+                if (
+                    isinstance(parsed_check, CodeElementCheck)
+                    and parsed_check.check_kind == INVARIANT
                 ):
-                    raise PreprocessorError(
-                        f"{parsed_check.check_kind} annotation is not allowed here",
-                        code_elem.location,
-                    )
-
-            if isinstance(parsed_check, CodeElementLogicalVariableDeclaration):
-                self.add_logical_variable(parsed_check)
-            elif isinstance(parsed_check, CodeElementStorageUpdate):
-                self.add_state_change(parsed_check)
-            elif isinstance(parsed_check, CodeElementCheck):
-                is_post = parsed_check.check_kind == POST_COND
-                z3_transformer = Z3Transformer(
-                    self.identifiers,
-                    self,
-                    self.logical_identifiers,
-                    self.storage_vars,
-                    is_post,
-                )
-                expr = z3_transformer.visit(parsed_check.formula)
-                annotation = Annotation(
-                    sexpr=expr, source=[parsed_check.unpreprocessed_rep]
-                )
-
-                if parsed_check.check_kind == INVARIANT:
-                    append_check(
-                        parsed_check.check_kind,
-                        self.current_scope + code_elem.identifier.name,
-                        annotation,
+                    if not isinstance(code_elem, CodeElementLabel):
+                        raise PreprocessorError(
+                            "@invariant annotation must be placed before a label",
+                            code_elem.location,
+                        )
+                elif isinstance(parsed_check, CodeElementCheck):
+                    if not (
+                        isinstance(code_elem, CodeElementFunction)
+                        and code_elem.element_type == "func"
+                    ):
+                        raise PreprocessorError(
+                            f"{parsed_check.check_kind} annotation is not allowed here",
+                            code_elem.location,
+                        )
+
+                if isinstance(parsed_check, CodeElementLogicalVariableDeclaration):
+                    self.add_logical_variable(parsed_check)
+                elif isinstance(parsed_check, CodeElementStorageUpdate):
+                    self.add_state_change(parsed_check)
+                elif isinstance(parsed_check, CodeElementCheck):
+                    is_post = parsed_check.check_kind == POST_COND
+                    z3_transformer = Z3Transformer(
+                        self.identifiers,
+                        self,
+                        self.logical_identifiers,
+                        self.storage_vars,
+                        is_post,
                     )
-                elif parsed_check.check_kind in (PRE_COND, POST_COND):
-                    append_check(
-                        parsed_check.check_kind,
-                        None,
-                        annotation,
+                    expr = z3_transformer.visit(parsed_check.formula)
+                    annotation = Annotation(
+                        sexpr=expr, source=[parsed_check.unpreprocessed_rep]
                     )
 
+                    if parsed_check.check_kind == INVARIANT:
+                        append_check(
+                            parsed_check.check_kind,
+                            self.current_scope + code_elem.identifier.name,
+                            annotation,
+                        )
+                    elif parsed_check.check_kind in (PRE_COND, POST_COND):
+                        append_check(
+                            parsed_check.check_kind,
+                            None,
+                            annotation,
+                        )
+            except MissingIdentifierError as e:
+                raise PreprocessorError(str(e), location=parsed_check.location)
+
         self.current_checks = []
 
     def visit_function_body_with_retries(