Skip to content

Commit

Permalink
Enable code quality checks (#115)
Browse files Browse the repository at this point in the history
* rust-lite/: adjustments for code-quality checks

* src/{rust-lite,tests}: fix remaining code quality check issues

* .github/build-and-test: add code quality test step

* Dockerfile: enable poetry install on Docker image

* Dockerfile: add curl

* Dockerfile: setup path for poetry

* rust-lite/{manager,__main__}: remove added function

* rust-lite/__main__: undo use of _LOGGER

---------

Co-authored-by: ACassimiro <[email protected]>
  • Loading branch information
ehildenb and ACassimiro authored Oct 7, 2024
1 parent 3033bb4 commit b0d2398
Show file tree
Hide file tree
Showing 8 changed files with 75 additions and 66 deletions.
19 changes: 19 additions & 0 deletions .github/workflows/build-and-test.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,25 @@
cancel-in-progress: true

jobs:
code-quality:
name: 'Code Quality Checks'
runs-on: [self-hosted, linux, normal]
steps:
- name: 'Check out code'
uses: actions/checkout@v3
with:
submodules: recursive
- name: 'Set up Docker'
uses: ./.github/actions/with-docker
with:
container-name: k-rust-demo-${{ github.sha }}
- name: 'Python Code Quality Checks'
run: docker exec -t k-rust-demo-${{ github.sha }} /bin/bash -c 'make -C rust-lite'
- name: 'Tear down Docker'
if: always()
run: |
docker stop k-rust-demo-${{ github.sha }}
build-test:
name: 'Build And Test'
runs-on: [self-hosted, linux, normal]
Expand Down
13 changes: 6 additions & 7 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_COMMIT}

COPY --from=Z3 /usr/bin/z3 /usr/bin/z3

# RUN apt-get update \
# && apt-get upgrade --yes \
# && apt-get install --yes \
RUN apt-get update \
&& apt-get upgrade --yes \
&& apt-get install --yes \
curl
# cmake \
# curl \
# pandoc \
# python3 \
# python3-pip \
Expand All @@ -26,11 +26,10 @@ RUN groupadd -g $GROUP_ID user && useradd -m -u $USER_ID -s /bin/sh -g user user
USER user:user
WORKDIR /home/user

# RUN curl -sSL https://install.python-poetry.org | python3 - \
# && poetry --version
RUN curl -sSL https://install.python-poetry.org | python3 - --version 1.7.1

# RUN pip3 install --user \
# cytoolz \
# numpy

# ENV PATH=/home/user/wabt/build:/home/user/.local/bin:$PATH
ENV PATH=/home/user/.local/bin:$PATH
2 changes: 1 addition & 1 deletion rust-lite/src/rust_lite/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '0.1.0'
VERSION: Final = '0.1.0'
21 changes: 12 additions & 9 deletions rust-lite/src/rust_lite/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -3,20 +3,18 @@
import logging
import sys
from collections.abc import Iterable
from typing import TYPE_CHECKING
from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
from pyk.cli.pyk import parse_toml_args
from pathlib import Path
from typing import TYPE_CHECKING, Any

from pyk.cli.pyk import parse_toml_args

from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
from .manager import RustLiteManager

from . import VERSION

if TYPE_CHECKING:
from argparse import Namespace
from collections.abc import Callable, Iterator
from typing import Any, Final, TypeVar
from typing import Final, TypeVar

from .cli import RunOptions

T = TypeVar('T')
Expand Down Expand Up @@ -61,24 +59,29 @@ def exec_run(options: RunOptions) -> None:

module_manager.print_k_top_element()

def trigger_exec_run(stripped_args):

def trigger_exec_run(stripped_args: dict[str, Any]) -> None:
options = generate_options(stripped_args)
executor_name = 'exec_run'
execute = globals()[executor_name]
execute(options)


def exec_empty() -> None:
stripped_args = {'command': 'run', 'input_file': Path('../tests/preprocessing/empty.rs')}
trigger_exec_run(stripped_args)


def exec_erc20() -> None:
stripped_args = {'command': 'run', 'input_file': Path('../tests/syntax/erc_20_token.rs')}
trigger_exec_run(stripped_args)


def exec_staking() -> None:
stripped_args = {'command': 'run', 'input_file': Path('../tests/syntax/staking.rs')}
trigger_exec_run(stripped_args)


def exec_lending() -> None:
stripped_args = {'command': 'run', 'input_file': Path('../tests/syntax/lending.rs')}
trigger_exec_run(stripped_args)
Expand All @@ -91,4 +94,4 @@ def _loglevel(args: Namespace) -> int:
if args.verbose:
return logging.INFO

return logging.WARNING
return logging.WARNING
25 changes: 9 additions & 16 deletions rust-lite/src/rust_lite/cli.py
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,8 @@
from typing import TYPE_CHECKING, Any

from pyk.cli.args import DisplayOptions as PykDisplayOptions
from pyk.cli.args import KCLIArgs, KDefinitionOptions, LoggingOptions, Options, SaveDirOptions
from pyk.cli.args import KCLIArgs, KDefinitionOptions, LoggingOptions, Options
from pyk.cli.utils import file_path
from pyk.kast.inner import KSort
from pyk.kore.tools import PrintOutput
from pyk.ktool.krun import KRunOutput

if TYPE_CHECKING:
from collections.abc import Callable
Expand Down Expand Up @@ -135,9 +132,8 @@ def from_option_string() -> dict[str, str]:
def get_argument_type() -> dict[str, Callable]:
return LoggingOptions.get_argument_type()

class RunOptions(
LoggingOptions
):

class RunOptions(LoggingOptions):
input_file: Path

@staticmethod
Expand All @@ -148,17 +144,14 @@ def default() -> dict[str, Any]:

@staticmethod
def from_option_string() -> dict[str, str]:
return (
LoggingOptions.from_option_string()
)
return LoggingOptions.from_option_string()

@staticmethod
def get_argument_type() -> dict[str, Callable]:
return (
{
'input_file': file_path,
}
)
return {
'input_file': file_path,
}


class RustLiteCLIArgs(KCLIArgs):
@cached_property
Expand All @@ -183,4 +176,4 @@ def display_args(self) -> ArgumentParser:
action='store_true',
help='Sort collections before outputting term.',
)
return args
return args
51 changes: 26 additions & 25 deletions rust-lite/src/rust_lite/manager.py
Original file line number Diff line number Diff line change
@@ -1,27 +1,29 @@
from __future__ import annotations

import pprint
from collections.abc import Iterable
from collections import deque
from typing import TYPE_CHECKING, Mapping, Any
from pathlib import Path
from typing import TYPE_CHECKING

from pyk.kast.inner import KApply, KSequence, KSort, KToken, KInner
from pyk.kast.parser import KAstParser
from pyk.kast.manip import set_cell
from pyk.cterm import CTerm
from pyk.ktool.krun import KRun
from pyk.kast.inner import KApply, KSequence
from pyk.kast.manip import set_cell
from pyk.kast.parser import KAstParser
from pyk.ktool.kprint import _kast
from pyk.ktool.krun import KRun
from pyk.prelude.k import GENERATED_TOP_CELL

if TYPE_CHECKING:
from pyk.kast.inner import KInner

_PPRINT = pprint.PrettyPrinter(width=41, compact=True)

class RustLiteManager():

class RustLiteManager:
krun: KRun
cterm: CTerm

def __init__(self) -> None:
dir_path = Path(f'../.build/mx-rust-testing-kompiled')
dir_path = Path('../.build/mx-rust-testing-kompiled')
self.krun = KRun(dir_path)
self._init_cterm()

Expand All @@ -32,39 +34,38 @@ def _init_cterm(self) -> None:

def load_program(self, program_path: str) -> None:

returned_process = _kast(file=program_path, definition_dir=f'../.build/rust-preprocessing-kompiled')
returned_process = _kast(file=program_path, definition_dir='../.build/rust-preprocessing-kompiled')

program = returned_process.stdout

parser = KAstParser(program)
parsed_program = parser.klist()

self.cterm = CTerm.from_kast(set_cell(self.cterm.config, 'K_CELL', KSequence(KApply('crateParser(_)_RUST-PREPROCESSING-SYNTAX_Initializer_Crate', parsed_program))))
self.cterm = CTerm.from_kast(
set_cell(
self.cterm.config,
'K_CELL',
KSequence(KApply('crateParser(_)_RUST-PREPROCESSING-SYNTAX_Initializer_Crate', parsed_program)),
)
)
pattern = self.krun.kast_to_kore(self.cterm.config, sort=GENERATED_TOP_CELL)
output_kore = self.krun.run_pattern(pattern, pipe_stderr=False)
self.cterm = CTerm.from_kast(self.krun.kore_to_kast(output_kore))
def fetch_k_cell_content(self) -> KToken:

def fetch_k_cell_content(self) -> KInner:
cell = self.cterm.cell('K_CELL')
return cell

def print_k_top_element(self) -> None:
cell = self.fetch_k_cell_content()
queue: deque[KInner] = deque(cell)

k_cell_contents = cell.items if isinstance(cell, KSequence) else [cell]
print('--------------------------------------------------')
print('K CELL TOP ELEMENT: ')
if(len(queue) > 0):
top_cell = queue.popleft()
_PPRINT.pprint(top_cell)
else:
print('Cell is empty.')
for cell_content in k_cell_contents:
_PPRINT.pprint(cell_content)


def print_constants_cell(self) -> None:
cell = self.cterm.cell('CONSTANTS_CELL')

print('--------------------------------------------------')
print('CONSTANTS CELL ELEMENT: ')
_PPRINT.pprint(cell)

5 changes: 1 addition & 4 deletions rust-lite/src/tests/integration/test_integration.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,2 @@
from rust_lite.hello import hello


def test_hello() -> None:
assert hello('World') == 'Hello, World!'
assert True
5 changes: 1 addition & 4 deletions rust-lite/src/tests/unit/test_unit.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,2 @@
from rust_lite.hello import hello


def test_hello() -> None:
assert hello('World') == 'Hello, World!'
assert True

0 comments on commit b0d2398

Please sign in to comment.