diff --git a/.github/workflows/test-pytest.yml b/.github/workflows/test-pytest.yml new file mode 100644 index 0000000..fa349e2 --- /dev/null +++ b/.github/workflows/test-pytest.yml @@ -0,0 +1,38 @@ +name: Run pytest + +on: [push] + +env: + PYTHON_VERSION: "3.11" + POETRY_VERSION: "1.4.2" + POETRY_URL: https://install.python-poetry.org + +jobs: + run-pytest: + runs-on: ubuntu-latest + steps: + - name: Checkout + uses: actions/checkout@v3 + - name: Set up Python ${{ env.PYTHON_VERSION }} + uses: actions/setup-python@v4 + with: + python-version: ${{ env.PYTHON_VERSION }} + id: setup_python + - name: Cache Poetry cache + uses: actions/cache@v3 + with: + path: ~/.cache/pypoetry + key: poetry-cache-${{ runner.os }}-${{ steps.setup_python.outputs.python-version }}-${{ env.POETRY_VERSION }} + - name: Cache Packages + uses: actions/cache@v3 + with: + path: ~/.local + key: poetry-local-${{ runner.os }}-${{ steps.setup_python.outputs.python-version }}-${{ hashFiles('**/poetry.lock') }}-${{ hashFiles('.github/workflows/*.yml') }} + - name: Install Poetry ${{ env.POETRY_VERSION }} + run: | + curl -sSL ${{ env.POETRY_URL }} | python - --version ${{ env.POETRY_VERSION }} + echo "$HOME/.local/bin" >> $GITHUB_PATH + - name: Install Dependencies + run: poetry install + - name: Run pytest + run: poetry run pytest diff --git a/tests/test_remove.py b/tests/test_remove.py new file mode 100644 index 0000000..975ee75 --- /dev/null +++ b/tests/test_remove.py @@ -0,0 +1,107 @@ +from textwrap import dedent +from verified_cogen.runners.validating import remove_asserts_and_invariants + + +def test_remove_line(): + code = dedent( + """\ + method main() { + assert a == 1; // assert-line + }""" + ) + assert remove_asserts_and_invariants(code) == dedent( + """\ + method main() { + }""" + ) + + +def test_remove_multiline_assert(): + code = dedent( + """\ + method main() { + // assert-start + assert a == 1 by { + + } + // assert-end + }""" + ) + assert remove_asserts_and_invariants(code) == dedent( + """\ + method main() { + }""" + ) + + +def test_remove_invariants(): + code = dedent( + """\ + method main() { + while true + // invariants-start + invariant false + invariant true + // invariants-end + { + } + }""" + ) + assert remove_asserts_and_invariants(code) == dedent( + """\ + method main() { + while true + { + } + }""" + ) + + +def test_remove_all(): + code = dedent( + """\ + method is_prime(k: int) returns (result: bool) + requires k >= 2 + ensures result ==> forall i :: 2 <= i < k ==> k % i != 0 + ensures !result ==> exists j :: 2 <= j < k && k % j == 0 + { + var i := 2; + result := true; + while i < k + // invariants-start + invariant 2 <= i <= k + invariant !result ==> exists j :: 2 <= j < i && k % j == 0 + invariant result ==> forall j :: 2 <= j < i ==> k % j != 0 + // invariants-end + { + if k % i == 0 { + result := false; + } + assert result ==> forall j :: 2 <= j < i ==> k % j != 0; // assert-line + // assert-start + assert !result ==> exists j :: 2 <= j < i && k % j == 0 by { + assert true; + } + // assert-end + i := i + 1; + } + }""" + ) + assert remove_asserts_and_invariants(code) == dedent( + """\ + method is_prime(k: int) returns (result: bool) + requires k >= 2 + ensures result ==> forall i :: 2 <= i < k ==> k % i != 0 + ensures !result ==> exists j :: 2 <= j < k && k % j == 0 + { + var i := 2; + result := true; + while i < k + { + if k % i == 0 { + result := false; + } + i := i + 1; + } + }""" + ) diff --git a/verified_cogen/runners/validating.py b/verified_cogen/runners/validating.py index 79c49cc..63fa5b9 100644 --- a/verified_cogen/runners/validating.py +++ b/verified_cogen/runners/validating.py @@ -7,7 +7,9 @@ from verified_cogen.runners.invariants import InvariantRunner # Regular expression to match Dafny method definitions -method_pattern = re.compile(r'method\s+(\w+)\s*\((.*?)\)\s*returns\s*\((.*?)\)(.*?)\{', re.DOTALL) +method_pattern = re.compile( + r"method\s+(\w+)\s*\((.*?)\)\s*returns\s*\((.*?)\)(.*?)\{", re.DOTALL +) def generate_validators(dafny_code: str) -> str: @@ -34,7 +36,9 @@ def generate_validators(dafny_code: str) -> str: returns = match.group(3) specs = match.group(4) - validator = f"method {method_name}_valid({parameters}) returns ({returns}){specs}" + validator = ( + f"method {method_name}_valid({parameters}) returns ({returns}){specs}" + ) validator += "{ var ret := " validator += f"{method_name}({', '.join(param.split(':')[0].strip() for param in parameters.split(',') if param.strip())});" @@ -43,23 +47,23 @@ def generate_validators(dafny_code: str) -> str: validators.append(validator) - return '\n'.join(validators) + return "\n".join(validators) def remove_asserts_and_invariants(dafny_code: str) -> str: patterns = [ - r'// assert-line.*\n', - r'// assert-start.*?// assert-end\n', - r'// invariants-start.*?// invariants-end\n' + r" *// assert-start.*?// assert-end\n", + r" *// invariants-start.*?// invariants-end\n", ] - combined_pattern = '|'.join(patterns) - cleaned_code = re.sub(combined_pattern, '', dafny_code, flags=re.DOTALL) - cleaned_code = re.sub(r'\n\s*\n', '\n', cleaned_code) - return cleaned_code.strip() + combined_pattern = "|".join(patterns) + cleaned_code = re.sub(combined_pattern, "", dafny_code, flags=re.DOTALL) + cleaned_code = re.sub(r"\n\s*\n", "\n", cleaned_code) + lines = cleaned_code.split("\n") + lines = [line for line in lines if "// assert-line" not in line] + return "\n".join(lines).strip() class ValidatingRunner(Runner): - @classmethod def _add_validators(cls, prg: str, inv_prg: str): validators = generate_validators(prg) @@ -80,7 +84,9 @@ def produce(cls, llm: LLM, prg: str) -> str: @classmethod def insert(cls, llm: LLM, prg: str, checks: str, mode: Mode) -> str: - return ValidatingRunner._add_validators(prg, InvariantRunner.insert(llm, prg, checks, mode)) + return ValidatingRunner._add_validators( + prg, InvariantRunner.insert(llm, prg, checks, mode) + ) @classmethod def precheck(cls, prg: str, mode: Mode):