Skip to content

Commit

Permalink
Merge pull request #35 from NethermindEth/ElijahVlasov/0.10.1-bump
Browse files Browse the repository at this point in the history
`cairo-lang==0.10.1` bump
  • Loading branch information
ElijahVlasov authored Nov 28, 2022
2 parents 0211aed + 80a47ed commit 9bb937e
Show file tree
Hide file tree
Showing 49 changed files with 1,322 additions and 1,092 deletions.
814 changes: 429 additions & 385 deletions poetry.lock

Large diffs are not rendered by default.

6 changes: 3 additions & 3 deletions pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ skip_gitignore = true

[tool.poetry]
name = "horus-compile"
version = "0.0.6.1"
version = "0.0.6.2"
authors = ["Nethermind <[email protected]>"]
description = "Use formally verified annotations in your Cairo code"
classifiers = [
Expand All @@ -33,12 +33,12 @@ horus-compile = "horus.compiler.horus_compile:run"

[tool.poetry.dependencies]
python = ">=3.7,<3.10"
cairo-lang = "0.9.1"
cairo-lang = "0.10.1"
marshmallow-dataclass = ">=7.1.0,<8.5.4"
eth-utils = "^1.2.0"
marshmallow = "^3.15.0"
z3-solver = "^4.8.15"
lark-parser = "^0.12.0"
lark = "^1.1.4"

[tool.poetry.dev-dependencies]
isort = "*"
Expand Down
7 changes: 6 additions & 1 deletion src/horus/compiler/code_elements.py
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
from __future__ import annotations

import dataclasses
from enum import Enum
from typing import Optional, Sequence
Expand All @@ -6,7 +8,7 @@
from starkware.cairo.lang.compiler.ast.cairo_types import CairoType
from starkware.cairo.lang.compiler.ast.code_elements import CodeElement
from starkware.cairo.lang.compiler.ast.expr import ArgList, Expression
from starkware.cairo.lang.compiler.ast.formatting_utils import LocationField
from starkware.cairo.lang.compiler.ast.formatting_utils import LocationField, Particle
from starkware.cairo.lang.compiler.ast.node import AstNode
from starkware.cairo.lang.compiler.error_handling import Location
from starkware.python.expression_string import ExpressionString
Expand All @@ -27,6 +29,9 @@ def to_expr_str(self) -> ExpressionString:
def get_children(self) -> Sequence[Optional["AstNode"]]:
return []

def get_particles(self) -> list[Particle]:
return []


@dataclasses.dataclass
class BoolFormula(AstNode):
Expand Down
5 changes: 3 additions & 2 deletions src/horus/compiler/parser.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@

import lark
from lark.exceptions import LarkError, UnexpectedToken, VisitError
from lark.load_grammar import PackageResource
from starkware.cairo.lang.compiler.error_handling import InputFile, LocationError
from starkware.cairo.lang.compiler.parser import wrap_lark_error
from starkware.cairo.lang.compiler.parser_transformer import ParserContext
Expand All @@ -13,7 +14,7 @@


def starkware_grammar_loader(
base_path: Union[None, str, lark.PackageResource], grammar_path: str
base_path: Union[None, str, PackageResource], grammar_path: str
) -> tuple[str, str]:
"""
A hack to load cairo.ebnf instead of cairo.lark.
Expand Down Expand Up @@ -45,7 +46,7 @@ def starkware_grammar_loader(
"typed_identifier",
"annotation",
],
lexer="standard",
lexer="basic",
parser="lalr",
propagate_positions=True,
import_paths=[starkware_grammar_loader],
Expand Down
14 changes: 8 additions & 6 deletions src/horus/compiler/parser_transformer.py
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,10 @@ def __init__(
super().__init__(input_file, parser_context)

@lark.v_args(meta=True)
def commented_code_element(self, value, meta):
comment: Optional[str] = value[1][1:] if len(value) == 2 else None
def commented_code_element(self, meta, value):
comment: Optional[str] = (
value[1][2:] if len(value) == 2 and value[1] is not None else None
)

if comment is not None:
possible_annotation = comment.strip()
Expand All @@ -65,16 +67,16 @@ def commented_code_element(self, value, meta):
expected_type=CodeElementAnnotation,
parser_context=self.parser_context,
)
code_elem = super().commented_code_element(value[:1], meta)
code_elem = super().commented_code_element(meta, [value[0], None])
code_elem.code_elm = AnnotatedCodeElement(
check, code_elm=code_elem.code_elm
)
return code_elem

return super().commented_code_element(value, meta)
return super().commented_code_element(meta, value)

@lark.v_args(meta=True)
def logical_identifier(self, value, meta):
def logical_identifier(self, meta, value):
identifier_name = ".".join(x.value for x in value)
if value[0].value == "$Return":
return ExprIdentifier(name=identifier_name, location=self.meta2loc(meta))
Expand All @@ -84,7 +86,7 @@ def logical_identifier(self, value, meta):
)

@lark.v_args(meta=True)
def logical_identifier_def(self, value, meta):
def logical_identifier_def(self, meta, value):
if value[0].value == "$Return":
raise ParserError(
f"'$Return' is a reserved name.", location=self.meta2loc(meta)
Expand Down
23 changes: 8 additions & 15 deletions src/horus/compiler/preprocessor.py
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,6 @@ def get_program(self) -> HorusProgram:
storage_vars[storage_var] = self.get_size(
TypeStruct(
self.identifiers.get(storage_var + "read" + "Args").canonical_name,
is_fully_resolved=True,
)
)

Expand Down Expand Up @@ -117,17 +116,9 @@ def add_logical_variable(
declaration: CodeElementLogicalVariableDeclaration,
is_member: bool = False,
):
declaration.type = self.resolve_type(declaration.type)
if isinstance(declaration.type, TypeStruct):
if declaration.type.is_fully_resolved:
search_result = self.identifiers.get(declaration.type.scope)
else:
search_result = self.identifiers.search(
self.accessible_scopes, declaration.type.scope
)
definition = resolve_search_result(search_result, self.identifiers)

declaration.type.scope = definition.full_name
declaration.type.is_fully_resolved = True
definition = self.identifiers.get_by_full_name(declaration.type.scope)

assert isinstance(
definition, StructDefinition
Expand All @@ -148,7 +139,9 @@ def add_logical_variable(
else:
member_name = f"{declaration.name}.{i}"
self.add_logical_variable(
CodeElementLogicalVariableDeclaration(member_name, member.typ),
CodeElementLogicalVariableDeclaration(
member_name, self.resolve_type(member.typ)
),
is_member=True,
)

Expand All @@ -159,7 +152,7 @@ def add_logical_variable(
variables_of_the_function = current_annotations.logical_variables
variables_of_the_function[
ScopedName.from_string(declaration.name)
] = declaration.type
] = self.resolve_type(declaration.type)
self.specifications[self.current_scope] = current_annotations

self.logical_identifiers[declaration.name] = declaration.type
Expand All @@ -169,8 +162,8 @@ def add_state_change(self, decl: CodeElementStorageUpdate):
self.identifiers,
self,
self.logical_identifiers,
self.storage_vars,
is_post=True,
storage_vars=self.storage_vars,
)
z3_expr_transformer = Z3ExpressionTransformer(
identifiers=self.identifiers, z3_transformer=z3_transformer
Expand Down Expand Up @@ -287,8 +280,8 @@ def append_check(
self.identifiers,
self,
self.logical_identifiers,
is_post,
self.storage_vars,
is_post,
)
expr = z3_transformer.visit(parsed_check.formula)

Expand Down
Loading

0 comments on commit 9bb937e

Please sign in to comment.