Update dependency: deps/llvm-backend_release (#4624)

Co-authored-by: devops <[email protected]>
Co-authored-by: Theodoros Kasampalis <[email protected]>

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.84
+0.1.88

flake.nix

@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.84";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.88";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.76";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

pyk/src/tests/integration/kllvm/test_prooftrace.py

@@ -97,13 +97,13 @@ def test_proof_trace(self, hints: bytes, header: prooftrace.KoreHeader, definiti
     def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file: Path) -> None:
         # read the hints file and get the iterator for the proof trace
         it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header)
-        assert it.version == 12
+        assert it.version == 13
 
         # Test that the __iter__ is working
         list_of_events = list(it)
 
         # Test length of the list
-        assert len(list_of_events) == 13
+        assert len(list_of_events) == 14
 
         # Test the type of the events
         for event in list_of_events:
@@ -126,7 +126,7 @@ def test_streaming_parser_next(self, header: prooftrace.KoreHeader, hints_file:
 
         # read the hints file and get the iterator for the proof trace
         it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header)
-        assert it.version == 12
+        assert it.version == 13
 
         # skip pre-trace events
         while True:
@@ -189,8 +189,8 @@ def test_parse_proof_hint_single_rewrite(
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization event
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -259,8 +259,8 @@ def test_parse_proof_hint_reverse_no_ints(
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 9 post-initial-configuration events
         assert len(pt.trace) == 9
@@ -384,11 +384,11 @@ def test_parse_proof_hint_non_rec_function(
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
-        # 4 post-initial-configuration events
-        assert len(pt.trace) == 4
+        # 6 post-initial-configuration events
+        assert len(pt.trace) == 6
 
         # Contents of the k cell in the initial configuration
         kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern)
@@ -407,27 +407,32 @@ def test_parse_proof_hint_non_rec_function(
         assert len(rule_event.substitution) == 3
 
         # Functional event
-        fun_event = pt.trace[1].step_event
+        inner_fun_event = pt.trace[1].step_event
+        assert isinstance(inner_fun_event, prooftrace.LLVMFunctionEvent)
+        assert inner_fun_event.relative_position == '0:0:0:0'
+
+        # Simplification rule
+        inner_rule_event = pt.trace[2].step_event
+        assert isinstance(inner_rule_event, prooftrace.LLVMRuleEvent)
+
+        # Functional event
+        fun_event = pt.trace[3].step_event
         assert isinstance(fun_event, prooftrace.LLVMFunctionEvent)
         assert fun_event.name == "Lblid'LParUndsRParUnds'NON-REC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo{}"
         assert fun_event.relative_position == '0:0:0'
-        assert len(fun_event.args) == 2
-        # Check that arguments are a functional event and simplification rule
-        assert isinstance(fun_event.args[0].step_event, prooftrace.LLVMFunctionEvent)
-        assert fun_event.args[0].step_event.relative_position == '0:0:0:0'
-        assert isinstance(fun_event.args[1].step_event, prooftrace.LLVMRuleEvent)
+        assert len(fun_event.args) == 0
 
         # Then rule
-        rule_event = pt.trace[2].step_event
+        rule_event = pt.trace[4].step_event
         assert isinstance(rule_event, prooftrace.LLVMRuleEvent)
         axiom = repr(definition.get_axiom_by_ordinal(rule_event.rule_ordinal))
         axiom_expected = get_pattern_from_ordinal(definition_text, rule_event.rule_ordinal)
         assert axiom == axiom_expected
         assert len(rule_event.substitution) == 1
 
         # Then pattern
-        assert pt.trace[3].is_kore_pattern()
-        kore_pattern = llvm_to_pattern(pt.trace[3].kore_pattern)
+        assert pt.trace[5].is_kore_pattern()
+        kore_pattern = llvm_to_pattern(pt.trace[5].kore_pattern)
         k_cell = kore_pattern.patterns[0].dict['args'][0]
         assert k_cell['name'] == 'kseq'
         assert (
@@ -462,8 +467,8 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader,
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 3 post-initial-configuration events
         assert len(pt.trace) == 3
@@ -490,18 +495,12 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader,
         assert isinstance(hook_event, prooftrace.LLVMHookEvent)
         assert hook_event.name == 'INT.add'
         assert hook_event.relative_position == '0:0:0:0'
-        assert len(hook_event.args) == 3
-
-        fun_event = hook_event.args[0].step_event
-        assert isinstance(fun_event, prooftrace.LLVMFunctionEvent)
-        assert fun_event.name == "Lbl'UndsPlus'Int'Unds'{}"
-        assert fun_event.relative_position == '0:0:0:0'
-        assert len(fun_event.args) == 0
+        assert len(hook_event.args) == 2
 
-        arg1 = hook_event.args[1]
+        arg1 = hook_event.args[0]
         assert arg1.is_kore_pattern()
 
-        arg2 = hook_event.args[2]
+        arg2 = hook_event.args[1]
         assert arg2.is_kore_pattern()
 
         # Then pattern
@@ -549,8 +548,8 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 37 post-initial-configuration events
         assert len(pt.trace) == 37
@@ -709,8 +708,8 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 1 post-initial-configuration event
         assert len(pt.trace) == 1
@@ -738,8 +737,8 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -767,8 +766,8 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 3 post-initial-configuration events
         assert len(pt.trace) == 3
@@ -806,11 +805,11 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 404 post-initial-configuration events
-        assert len(pt.trace) == 419
+        assert len(pt.trace) == 776
 
 
 class TestIMP5(ProofTraceTest):
@@ -910,8 +909,8 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 15 initialization events
-        assert len(pt.pre_trace) == 15
+        # 16 initialization events
+        assert len(pt.pre_trace) == 16
 
         # 2 post-initial-configuration events
         assert len(pt.trace) == 2
@@ -949,11 +948,11 @@ def test_parse_proof_hint_builtin_hook_events(
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
-        # 3 post-initial-configuration events
-        assert len(pt.trace) == 3
+        # 4 post-initial-configuration events
+        assert len(pt.trace) == 4
 
         # Contents of the k cell in the initial configuration
         kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern)
@@ -971,19 +970,22 @@ def test_parse_proof_hint_builtin_hook_events(
         repr(definition.get_axiom_by_ordinal(rule_ordinal))
         get_pattern_from_ordinal(definition_text, rule_ordinal)
 
-        # Hook event with a nested event
+        # Hook event (first argument of next hook event)
         assert isinstance(pt.trace[1].step_event, prooftrace.LLVMHookEvent)
         assert pt.trace[1].step_event.name == 'BOOL.not'
-        assert pt.trace[1].step_event.relative_position == '0:0:0'
-        assert len(pt.trace[1].step_event.args) == 2
-        arg1 = pt.trace[1].step_event.args[0].step_event
-        arg2 = pt.trace[1].step_event.args[1]
-        assert isinstance(arg1, prooftrace.LLVMHookEvent)
-        assert arg1.name == 'BOOL.not'
-        assert arg1.relative_position == '0:0:0:0'
-        assert len(arg1.args) == 1
-        assert arg1.args[0].is_kore_pattern()
-        assert arg2.is_kore_pattern()
+        assert pt.trace[1].step_event.relative_position == '0:0:0:0'
+        assert len(pt.trace[1].step_event.args) == 1
+        assert pt.trace[1].step_event.args[0].is_kore_pattern()
+        result = llvm_to_pattern(pt.trace[1].step_event.result)
+
+        # Hook event
+        assert isinstance(pt.trace[2].step_event, prooftrace.LLVMHookEvent)
+        assert pt.trace[2].step_event.name == 'BOOL.not'
+        assert pt.trace[2].step_event.relative_position == '0:0:0'
+        assert len(pt.trace[2].step_event.args) == 1
+        assert pt.trace[2].step_event.args[0].is_kore_pattern()
+        arg = llvm_to_pattern(pt.trace[2].step_event.args[0].kore_pattern)
+        assert arg.json == result.json
 
         # Final configuration
-        assert pt.trace[2].is_kore_pattern()
+        assert pt.trace[3].is_kore_pattern()

pyk/src/tests/integration/test_krun_proof_hints.py

@@ -30,17 +30,14 @@ class Test0Decrement(KRunTest, ProofTraceTest):
         LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()))))
     """
 
-    HINTS_OUTPUT = """version: 12
+    HINTS_OUTPUT = """version: 13
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
-  function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
   arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
 hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
 hook: MAP.unit Lbl'Stop'Map{} ()
-  function: Lbl'Stop'Map{} ()
 hook result: kore[Lbl'Stop'Map{}()]
 hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
-  function: Lbl'Unds'Map'Unds'{} ()
   arg: kore[Lbl'Stop'Map{}()]
   arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
 hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
@@ -50,12 +47,11 @@ class Test0Decrement(KRunTest, ProofTraceTest):
 function: LblinitKCell{} (0)
 rule: 100 1
   VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
+  arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
+hook result: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
 function: Lblproject'Coln'KItem{} (0:0)
-  hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
-    function: LblMap'Coln'lookup{} (0:0:0:0)
-    arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())]
-    arg: kore[\\dv{SortKConfigVar{}}("$PGM")]
-  hook result: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
 rule: 139 1
   VarK = kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()]
 function: LblinitGeneratedCounterCell{} (1)
@@ -77,8 +73,8 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH
         pt = prooftrace.LLVMRewriteTrace.parse(hints, header)
         assert pt is not None
 
-        # 11 initialization events
-        assert len(pt.pre_trace) == 11
+        # 12 initialization events
+        assert len(pt.pre_trace) == 12
 
         # 1 post-initial-configuration event
         assert len(pt.trace) == 1