From 313aaba720c58d9634b8ff315c5a33a3d9e5c55e Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 8 May 2024 16:22:00 -0300 Subject: [PATCH] Support NULL return from `requires` binding of `get_requires()` (#4326) The llvm function `get_requires()` can return either the Pattern in the requires clause or nullptr. However, our binding only accepted the first case, and this PR fixes that behavior by testing if the result of `axiom.requires` returned a pattern. If not, we return None instead of trying to convert None to a LLVM Pattern. A unit test was added to ensure this behavior was documented and tested. --- pyk/src/pyk/kllvm/utils.py | 4 +++- pyk/src/tests/integration/kllvm/test_utils.py | 11 ++++++++++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kllvm/utils.py b/pyk/src/pyk/kllvm/utils.py index f4f59d46ecc..e2580de1f0c 100644 --- a/pyk/src/pyk/kllvm/utils.py +++ b/pyk/src/pyk/kllvm/utils.py @@ -8,7 +8,9 @@ from ..kore.syntax import Axiom, Pattern -def get_requires(axiom: Axiom) -> Pattern: +def get_requires(axiom: Axiom) -> Pattern | None: llvm_axiom = convert.sentence_to_llvm(axiom) llvm_pattern = llvm_axiom.requires + if llvm_pattern is None: + return None return convert.llvm_to_pattern(llvm_pattern) diff --git a/pyk/src/tests/integration/kllvm/test_utils.py b/pyk/src/tests/integration/kllvm/test_utils.py index 221963e5e26..3ad81c3150c 100644 --- a/pyk/src/tests/integration/kllvm/test_utils.py +++ b/pyk/src/tests/integration/kllvm/test_utils.py @@ -17,6 +17,11 @@ r'W{}(VarA : SortInt{},\dv{SortInt{}}("1"))', r'axiom {} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(X{}(Y{}(kseq{}(inj{SortInt{}, SortKItem{}}(VarA : SortInt{}),dotk{}())), Z : SortGeneratedCounterCell{}),\equals{SortBool{}, SortGeneratedTopCell{}}(W{}(VarA : SortInt{},\dv{SortInt{}}("1")),\dv{SortBool{}}("true"))),\and{SortGeneratedTopCell{}}(X{}(Y{}(kseq{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("1")),dotk{}())),),\top{SortGeneratedTopCell{}}())) []', ), + ( + 'axiom2', + r'', + r'axiom {} \rewrites{SortGeneratedTopCell{}}(\and{SortGeneratedTopCell{}}(V{}(X{}(kseq{}(inj{SortFoo{}, SortKItem{}}(W{}(Y{}(VarX : SortInt{}))), A : SortK{})), B : SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}()), \and{SortGeneratedTopCell{}}(V{}(X{}(kseq{}(inj{SortFoo{}, SortKItem{}}(Y{}(Z{}(VarX : SortInt{}))), A : SortK{})), B : SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) []', + ), ) @@ -26,7 +31,11 @@ def test_get_requires(test_id: str, kore_requires: str, kore_axiom: str) -> None: # Given axiom = KoreParser(kore_axiom).axiom() - expected_requires = KoreParser(kore_requires).pattern() + + if kore_requires == '': + expected_requires = None + else: + expected_requires = KoreParser(kore_requires).pattern() # When actual_requires = get_requires(axiom)