Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Update dependency: deps/k_release #634

Merged
merged 10 commits into from
Sep 8, 2023

Conversation

rv-jenkins
Copy link
Contributor

No description provided.

@tothtamas28
Copy link
Collaborator

tothtamas28 commented Sep 6, 2023

Regression analysis

CI failure: https://github.com/runtimeverification/pyk/actions/runs/6091261943/job/16527607156?pr=634

Caused by: runtimeverification/haskell-backend#3637

Generate bug-report with

$ make test-integration TEST_ARGS+='-k "TestImpProof and test_execute[branch]" -n0 --bug-report'

Running execute with depth=4 from

<generatedTop>
  <T>
    <k>
      int $n , .Ids ; if ( _B:Bool ) { $n = 1 ; } else { $n = 2 ; }
    </k>
    <state>
      .Map
    </state>
  </T>
  GENERATED_COUNTER_CELL
</generatedTop>

results in a BranchingResult with next_states:

<generatedTop>
  <T>
    <k>
      { $n = 1 ; }
    </k>
    <state>
      $n |-> 0
    </state>
  </T>
  GENERATED_COUNTER_CELL:GeneratedCounterCell
</generatedTop>
#And { _B:Bool #Equals true }
<generatedTop>
  <T>
    <k>
      { $n = 2 ; }
    </k>
    <state>
      $n |-> 0
    </state>
  </T>
  GENERATED_COUNTER_CELL:GeneratedCounterCell
</generatedTop>
#And { _B:Bool #Equals false }

and due to the regression, additionally:

#False

@tothtamas28 tothtamas28 force-pushed the _update-deps/runtimeverification/k branch from bdf404c to 8ca7e0f Compare September 7, 2023 07:19
goodlyrottenapple added a commit to runtimeverification/haskell-backend that referenced this pull request Sep 7, 2023
Fix for change introduced by #3637, wherein branching could contain
bottom states which were not being pruned. (see
runtimeverification/pyk#634 (comment))
@tothtamas28 tothtamas28 force-pushed the _update-deps/runtimeverification/k branch from bd505ec to 9bf3227 Compare September 7, 2023 13:44
@@ -93,6 +93,7 @@ def cterm_execute(
next_state = CTerm.from_kast(self.kprint.kore_to_kast(er.state.kore))
_next_states = er.next_states if er.next_states is not None else []
next_states = [CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in _next_states]
next_states = [cterm for cterm in next_states if not cterm.is_bottom]
Copy link
Collaborator

@tothtamas28 tothtamas28 Sep 8, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is fine for a hotfix. @PetarMax, please open an issue for dropping it (or perhaps replacing it for an assertion) once runtimeverification/haskell-backend#3650 makes it's way through the pipeline.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@rv-jenkins rv-jenkins merged commit 390af0a into master Sep 8, 2023
@rv-jenkins rv-jenkins deleted the _update-deps/runtimeverification/k branch September 8, 2023 08:04
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 9, 2024
Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Baltoli pushed a commit to runtimeverification/k that referenced this pull request Apr 10, 2024
Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants