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

@@ -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)

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)