Skip to content

Commit

Permalink
Fix crash node deduplication. If a non-crash node is a duplicate of a…
Browse files Browse the repository at this point in the history
… crash node, check if the thread could be crashed, if so, crash that thread. Also fix the name (#147)

Co-authored-by: jayaprabhakar <jayaprabhakar@gmail.com>
  • Loading branch information
jp-fizzbee and jayaprabhakar authored Feb 11, 2025
1 parent a0a281d commit aad1bb7
Showing 1 changed file with 29 additions and 8 deletions.
37 changes: 29 additions & 8 deletions modelchecker/processor.go
Original file line number Diff line number Diff line change
Expand Up @@ -774,7 +774,11 @@ func (n *Node) Duplicate(other *Node, yield bool) {
return
}
if n.Name != "crash" && other.Name == "crash" {
other.Name = n.Name
if yield {
other.Name = "yield"
} else {
other.Name = n.Name
}
}
parent := n.Inbound[0].Node
other.Inbound = append(other.Inbound, n.Inbound[0])
Expand Down Expand Up @@ -1289,6 +1293,11 @@ func (p *Processor) processNode(node *Node) (bool, bool) {
// We will keep the enabled state in the node, during execution but have to be
// copied to the link/transition when attaching/merging similar to Fairness.
if other.Enabled || !node.Enabled {
if yield && other.Name == "crash" {
if p.shouldThreadCrash(other) {
p.crashThread(other)
}
}
node.Duplicate(other, yield)
return false, false
} else {
Expand All @@ -1301,6 +1310,11 @@ func (p *Processor) processNode(node *Node) (bool, bool) {
for _, hash := range hashes {
if other, ok := p.visited[hash]; ok {
if other.Enabled || !node.Enabled {
if yield && other.Name == "crash" {
if p.shouldThreadCrash(other) {
p.crashThread(other)
}
}
node.Duplicate(other, yield)
return false, true
}
Expand Down Expand Up @@ -1341,16 +1355,11 @@ func (p *Processor) processNode(node *Node) (bool, bool) {
p.YieldNode(node)
}
node.Name = "yield"
if node.Process.GetThreadsCount() == 0 || node.Process.Current == -1 || !*p.config.Options.CrashOnYield {
return false, false
}
frameName := node.Process.currentThread().Stack.RawArray()[0].Name

if p.config.ActionOptions[frameName] != nil && p.config.ActionOptions[frameName].CrashOnYield != nil && !p.config.ActionOptions[frameName].GetCrashOnYield() {
return false, false
if p.shouldThreadCrash(node) {
p.crashThread(node)
}

p.crashThread(node)
return false, false
}
return false, false
Expand Down Expand Up @@ -1845,6 +1854,18 @@ func (p *Processor) ResetEphemeralVariables(node *Node, oldRole *lib.Role) {
}
}

func (p *Processor) shouldThreadCrash(node *Node) bool {
if node.Process.GetThreadsCount() == 0 || node.Process.Current == -1 || !*p.config.Options.CrashOnYield {
return false
}
frameName := node.Process.currentThread().Stack.RawArray()[0].Name

if p.config.ActionOptions[frameName] != nil && p.config.ActionOptions[frameName].CrashOnYield != nil && !p.config.ActionOptions[frameName].GetCrashOnYield() {
return false
}
return true
}

func captureStackTrace() string {
if !enableCaptureStackTrace {
return ""
Expand Down

0 comments on commit aad1bb7

Please sign in to comment.