nickng/dingo-hunter

Static analyser for finding Deadlocks in Go

👋

dingo-hunter's Issues

sesstype -> CFSM conversion ignores self-loop

Conversion from a sesstype (graph of actions) into CFSMs ignores actions which loops directly back to its parent. e.g. Label X; Recv; Goto X; generates a state machine that does a one-shot receive.

This is due to the automatic creation of a new state for a receive transition, which covers ordinary case but not self-loop.

Instead, the conversion from sesstype to CFSM should detect self-loop and treat as a special case.

Question: How to analyse entire Project with this tool ?

When I run this command dingo-hunter cfsms --prefix deadlock mycom/rootdirectory
It gives the below error message

cannot import absolute path mycom/rootdirectory

no initial packages were loaded

How to solve this?

issues installing gong

Two issues

1. If I do "git clone ssh://github.com/nickng/gong.git" as in the README, I get "Permission denied (publickey)." with "git clone [email protected]:nickng/gong.git" it worked fine
2. Failure with "ghc Gong.hs"

thanks

$ cd gong; ghc Gong.hs
[1 of 9] Compiling GoTypes          ( GoTypes.hs, GoTypes.o )

GoTypes.hs:12:1: error:
    Could not find module ‘Unbound.LocallyNameless’
    Use -v to see a list of the files searched for.
   |
12 | import Unbound.LocallyNameless hiding (Generic)
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Migrate to go/packages

Similar to the migration of Go modules, the new go/packages supports non-mod and mod's way of loading packages as a coherence set of packages.

We should retire our use of package loading and use go/packages going forward for forward/backward compatibility.

Trouble running/installing

Hello!

I have been trying to use this tool using the CFSM approach, but I have not been able to.
I followed the instructions and I can't seem to run the line "dingo-hunter cfsms --prefix deadlock example/local-deadlock/main.go", it says that the dingo-hunter command is not found.
Additionally, the "go get -u github.com/nickng/dingo-hunter" at the end issues a "code in directory /home/afonso/go_projects/src/github.com/nickng/migo expects import "github.com/nickng/migo".
I'm not sure if I made any mistake following the installation process, but any help would be much appreciated.

Thank you!

Migrate to Go modules

With the arrival of go1.16 modules is on by default
We're not mod ready and should migrate

Some channel-closing programs are failed for the naming issue

This simple channel-closing program is failed with a Gong error Some of ["main.main.t0_0_0"] are not declared.

func main() {
    x := make(chan bool)
    close(x)
}

This Go program is translated into MiGo below:

def main.main():
    let t0 = newchan main.main.t0_0_0, 0;
    close main.main.t0_0_0;

I think this error occurred because the argument of close in MiGo is main.main.t0_0_0 instead of t0.

cfsms extraction panics when analysing undefined channel

Running cfsms on my code, I get a panic. See below a part of the output. I attach full output :

`
-- return from net.cgoLookupServicePort (2 retvals)
net.cgoLookupPort.t28 = extract t27[#0] == Undefined
net.cgoLookupPort.t29 = extract t27[#1] == net.cgoLookupServicePort.t47@0
New channel net.cgoLookupPort.t30@0 { type: net.portLookupResult } by net.cgoLookupPort.t30@0 at /usr/local/opt/go/libexec/src/net/cgo_unix.go:84:16
^ in role main
& changetype from net.cgoLookupPort.t30 to net.cgoLookupPort.t31 (channel net.cgoLookupPort.t30@0)
^ origin
@@ queue go net.cgoPortLookup(result:caller[net.cgoLookupPort.t31] = net.cgoLookupPort.t30@0 channel net.cgoLookupPort.t30@0, hints:caller[net.cgoLookupPort.t0] = net.cgoLookupPort.t0@0 struct, network:caller[net.cgoLookupPort.network] = Undefined, service:caller[net.cgoLookupPort.service] = Undefined)
++ invoke net.cgoLookupPort.ctx.func (context.Context).Done() <-chan struct{}
select net.cgoLookupPort.t30@0 (2 states)
Recv main←ᶜʰnet.cgoLookupPort.t30@0nondet
Called by: net.cgoLookupPort()
Called by: (*net.Resolver).lookupPort()
Called by: (*net.Resolver).LookupPort()
Called by: (*net.Resolver).internetAddrList()
Called by: net.ResolveUDPAddr()
Called by: github.com/socialpoint/edwin/vendor/github.com/socialpoint-labs/bsk/metrics.NewDataDog()
Called by: github.com/socialpoint/edwin/vendor/github.com/socialpoint-labs/bsk/metrics.NewMetricsRunnerFromDSN()
panic: Select: Channel net.cgoLookupPort.t32 at /usr/local/opt/go/libexec/src/net/cgo_unix.go:89:17 is undefined

goroutine 919 [running]:
github.com/nickng/dingo-hunter/cfsmextract.visitSelect(0xc436ba2180, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:328 +0xf37
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0x17d6c60, 0xc436ba2180, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:85 +0x39e
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc436b99760, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x7e
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc436b9e980, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:404 +0xacd
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0x17d6180, 0xc436b9e980, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:94 +0x97f
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc436b99290, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x7e
github.com/nickng/dingo-hunter/cfsmextract.visitJump(0xc436b8a438, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:480 +0x4b
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0x17d6360, 0xc436b8a438, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:97 +0x647
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc436b993f0, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x7e
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc436b9e780, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:399 +0xa01
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0x17d6180, 0xc436b9e780, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:94 +0x97f
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc436b991e0, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x7e
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc436b9e700, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:399 +0xa01
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0x17d6180, 0xc436b9e700, 0xc42f79c380)
/Users/dpinyol/socialpoint/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:94 +0x97f
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc436b988f0, 0xc42f79c380)
`

Error running example

Hello,
I am having some problems running some the example programs provided, namely the deadlocking-philosophers. When I try to generate a .migo file, it panics:

panic: runtime error: invalid memory address or nil pointer dereference
[signal SIGSEGV: segmentation violation code=0x1 addr=0x20 pc=0x7e7651]

goroutine 275 [running]:
github.com/nickng/dingo-hunter/migoextract.(*Const).String(0xc0027af200, 0xc000f80000, 0x70)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/instance.go:93 +0x31
github.com/nickng/dingo-hunter/migoextract.visitFunc(0xc005146f00, 0xc0028bb590, 0xc001977e10)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:28 +0x3fe
github.com/nickng/dingo-hunter/migoextract.(*Function).call(0xc001977860, 0xc008535fc0, 0xc005146f00, 0x0, 0x0, 0xc0028bb590, 0xc0059430e0, 0xc002ab7560, 0x2)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/call.go:304 +0xbb
github.com/nickng/dingo-hunter/migoextract.(*Function).callFn(0xc001977860, 0xc008535fc0, 0xc0028bb590, 0xc0059430e0, 0xc002ab7560, 0x60291c00)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/call.go:296 +0x73
github.com/nickng/dingo-hunter/migoextract.(*Function).Call(0xc001977860, 0xc008535f80, 0xc0028bb590, 0xc0059430e0, 0xc002ab7560)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/call.go:62 +0xe5
github.com/nickng/dingo-hunter/migoextract.visitCall(0xc008535f80, 0xc0028bb590, 0xc00115d360)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:268 +0x225
github.com/nickng/dingo-hunter/migoextract.visitInstr(0xce0720, 0xc008535f80, 0xc0028bb590, 0xc00115d360)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:87 +0x7cb
github.com/nickng/dingo-hunter/migoextract.visitBasicBlock(0xc008548370, 0xc0028bb590, 0xc001977860, 0xc0059430e0, 0xc002ab7560)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:76 +0x3f8
github.com/nickng/dingo-hunter/migoextract.visitIf(0xc00853efe0, 0xc0028bb590, 0xc00160f870)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:608 +0x43b
github.com/nickng/dingo-hunter/migoextract.visitInstr(0xce0f00, 0xc00853efe0, 0xc0028bb590, 0xc00115d870)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:105 +0x6fa
github.com/nickng/dingo-hunter/migoextract.visitBasicBlock(0xc0085482c0, 0xc0028bb590, 0xc001977860, 0xc005942d20, 0xc002ab7560)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:76 +0x3f8
github.com/nickng/dingo-hunter/migoextract.visitJump(0xc0084c3d48, 0xc0028bb590, 0xc00160fc10)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:839 +0x109f
github.com/nickng/dingo-hunter/migoextract.visitInstr(0xce10e0, 0xc0084c3d48, 0xc0028bb590, 0xc00115dc10)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:111 +0x3ee
github.com/nickng/dingo-hunter/migoextract.visitBasicBlock(0xc008548210, 0xc0028bb590, 0xc001977860, 0xc0059426e0, 0xc002ab7560)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:76 +0x3f8
github.com/nickng/dingo-hunter/migoextract.visitFunc(0xc005147680, 0xc0028bb590, 0xc001977860)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/visit.go:38 +0x596
github.com/nickng/dingo-hunter/migoextract.(*TypeInfer).Run(0xc0028bb590)
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/migoextract/migoextract.go:78 +0x990
created by github.com/nickng/dingo-hunter/cmd.extractMigo
	/home/afonso/go_projects/src/github.com/nickng/dingo-hunter/cmd/migo.go:83 +0x538

Any idea as to why this may be happening?
Thanks!

Errors when running examples

Hello,

I get some errors when running dingo-hunter on the programs from the examples folder.
I have contacted Nick about this, but he was busy and could not help me at the time.
Below is a summary of the errors, in the hope that someone can clarify if these are really errors related to the tool or if I'm doing anything wrong.
Thank you!

CFSMs errors:

• altbit - panic: Select: Channel main.rx.t12 is undefined
• dining-philosophers - panic: Select: Channel (*main.Philosopher).getChopsticks.t16 is undefined
• fcall - FATAL ERROR: (line 3) place q00q10q20q30q40 not declared
• multiple-files - Undeclared name: x ; couldn't load packages due to errors: main
• multiple-timeout - panic: Select: Channel main.main.t1 is undefined
• philo - Not exactly an error, but running for 10-15 minutes does not seem to be enough to show the full output.
• powsers - panic: Select: Channel main.getn.t21 is undefined
• timeout-behaviour - panic: Select: Channel main.main.t2 is undefined

MiGo Types errors:

• channel-scoping-test - Gong: Some of ["t0"] are not declared.
• deadlocking-philosophers - panic: runtime error: invalid memory address or nil pointer dereference
• dining-philosophers - panic: runtime error: invalid memory address or nil pointer dereference
• fanin-pattern - Gong: Some of ["t0", "t1", "t3"] are not declared.
• fanin-pattern-commaok - Gong: [unfoldTillGuard] We don't deal with Seq yet: main.fanin5 <t0, t1>; main.main#14 <t0, t11>; 0
• fcall - Gong: Some of ["t0"] are not declared.
• github-golang-go-issue-12734 - github-golang-go-issue-12734.migo is not fenced.
• golang-blog-prime-sieve - Gong: [unfoldTillGuard] We don't deal with Seq yet
• makechan-in-loop - Gong: Some of ["t12"] are not declared.
• md5 - panic: runtime error: invalid memory address or nil pointer dereference
• multi-makechan-same-var - Gong: Some of ["t0"] are not declared.
• multiple-files - Undeclared name: x ; couldn't load packages due to errors: main
• multiple-timeout - Gong: Something went wrong, can't find: main.main#1
• philo - Gong: Some of ["t5"] are not declared.
• powsers - Gong: Some of ["t32"] are not declared.
• producer-consumer - Gong: Some of ["done"] are not declared.
• ring-pattern - ring-pattern.migo is not fenced
• russ-cox-fizzbuzz - Gong: Some of ["t4", "t1"] are not declared.
• select-with-weak-mismatch - Gong: Something went wrong, can't find: main.main#1
• single-gortn-method-call - Gong: Some of ["t1"] are not declared.
• spawn-in-choice - panic: runtime error: invalid memory address or nil pointer dereference
• squaring-cancellation - Gong: Some of ["t3", "t0"] are not declared.
• squaring-fanin - Gong: Some of ["t11", "t2"] are not declared.
• squaring-fanin-bad - Gong: Some of ["t11", "t2"] are not declared.
• squaring-pipeline - Gong: Some of ["t4"] are not declared.
• struct-done-channel - Gong: Some of ["t1"] are not declared.

Unknown name issue when there are no instructions after if block or select block

When there are no (channel-related) instructions after if block or select block, the MiGo code is broken due to the unknown function name.

A sample code is the following

func main() {
    x := make(chan bool)
    go func() { x <- true }()
    if true {
        <-x
    }
}

This code is converted to:

def main.main():
    let t1 = newchan main.main.t1_0_0, 0;
    spawn main.main$1(t1);
    if recv t1; call main.main#2(t1); else endif;
def main.main$1(x):
    send x;

The problem is undefined main.main#2.

Run my project with panic

on centos7, I run commd:

~/workspace/Server/go/bin/dingo-hunter cfsms --prefix deadlock myproject/

to check deadlock end with panic output:

panic: Select: Channel net.cgoLookupPort.^[[4mt32^[[0m at /usr/local/go/src/net/cgo_unix.go:90:17 is undefined

goroutine 1255 [running]:
github.com/nickng/dingo-hunter/cfsmextract.visitSelect(0xc4289d2e40, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:328 +0x10e0
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0xe5f280, 0xc4289d2e40, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:85 +0x401
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc42d9dd6b0, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x81
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc4377c9820, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:404 +0xc1a
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0xe5e800, 0xc4377c9820, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:94 +0xb8d
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc42d9dcbb0, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x81
github.com/nickng/dingo-hunter/cfsmextract.visitJump(0xc42dedf368, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:480 +0x4d
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0xe5e9e0, 0xc42dedf368, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:97 +0x76e
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc42d9dce70, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x81
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc4377c95c0, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:399 +0xb3b
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0xe5e800, 0xc4377c95c0, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:94 +0xb8d
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc42d9dca50, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x81
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc4377c9500, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:399 +0xb3b
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0xe5e800, 0xc4377c9500, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:94 +0xb8d
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc4297a1550, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x81
github.com/nickng/dingo-hunter/cfsmextract.visitIf(0xc4377c8b60, 0xc426af0980)
/root/workspace/Server/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:399 +0xb3b
....

Closing a channel causes GMC synthesis to fail.

In the program below, because of the line where the channel is closed the following happen:

i) GMC synthesis fails.

ii) The global graph constructed ends up being simpler than when the channel is not closed. When the channel is not closed the global graph becomes very complex (contains many diamond and "|" nodes).

package main

func Sender(ch chan <- int, end chan <- bool) {
	ch <-42	
	close(ch)  // <------
	end <- true
}

func Receiver(ch <- chan int, end chan <- bool) {
	<-ch
	end <-true
}

func main() {
	ch := make(chan int)
	end := make(chan bool)
	go Sender(ch,end)
	go Receiver(ch,end)
	<-end
	<-end
}

readme usage example typos

At the Readme some command line are not up to date, for example the command

dingo-hunter infer example/local-deadlock/main.go --no-logging --output deadlock.migo

should be

dingo-hunter migo examples/local-deadlock/main.go --no-logging --output deadlock.migo

Impossible type assertion

Build fails on the latest go release (go1.5.3) with the following error:
sesstype/sesstype.go:37: impossible type assertion:
*"golang.org/x/tools/go/types".Chan does not implement "go/types".Type (wrong type for Underlying method)
have Underlying() "golang.org/x/tools/go/types".Type
want Underlying() "go/types".Type

The reason seems to be golang/tools@542ffc7

Temporarily workaround (before go1.6 release) is to build with go1.5

Φ-node where initial value is nil causes segfault

In a Φ-node where the initial value is a typed constant, e.g. nil:[]int, Φ register will be stored as a "Panic:..." string (because we get the name of the initial register as reg.Name()) but does not terminate the program. Later when the Φ register is used, it causes a segfault.

The Φ-node always come after the initial register's assignment so a workround is to special-case when a Φ-node with nil initial value is present (e.g. store as a dummy register rather than trying to resolve the name). The type can be used to generate a zero value for the initial register.

Revamp analyser to handle undefined channels without panicking

Panics should not be used for handling undefined channel variables.
The following should be tried before panicking:

• Use pointer analysis to find possible source of channel
• Dummy out a new channel variable on the fly if the channel is used in multiple places
• Flag as an error but continue analysis
• When initialising new struct, use zero value to fully initialise memory (not just the field being accessed)

can't analyze etcd

I try

[anthony@go/src/github.com/coreos/etcd]$ dingo-hunter main.go

and get (truncated):

++ call.toplevel init()
++ call.toplevel main()
++ call github.com/coreos/etcd/etcdmain.Main()
++ call github.com/coreos/etcd/etcdmain.checkSupportArch()
++ call os.LookupEnv(key:caller[???."ETCD_UNSUPPORTED_...":string] = Undefined)
++ call syscall.Getenv(key:caller[os.LookupEnv.key] = Undefined)
   # t0 = Alloc local string (value) of type string
   # t1 = Alloc local bool (found) of type bool
++ call (*sync.Once).Do()
-- return from (*sync.Once).Do (0 retvals)
++ call builtin len(key) # TODO (handle builtin)
   # t4 = t3 == 0:int
   # store *syscall.Getenv.t0 = ???."":string of type string
   # store *syscall.Getenv.t1 = ???.false:bool of type bool
   # *t0 = *local string (value) (not found)
   # *t1 = *local bool (found) (not found)
++ call (*sync.RWMutex).RLock()
-- return from (*sync.RWMutex).RLock (0 retvals)
   syscall.Getenv.t8 = *env (global) of type *map[string]int
    ^ i.e. ???.env@0
   # *env = *syscall.env/???.env (not found, type=map[string]int)
   # unhandled t9 = t8[key],ok
   # t10 = extract t9 #0 of type int
   # t11 = extract t9 #1 of type bool
   syscall.Getenv.t16 = *envs (global) of type *[]string
    ^ i.e. ???.envs@0
   syscall.Getenv.t16 = *envs (array)
   syscall.Getenv.t17 = &t16(=???.envs@0)[&{{{35341377088} 10 6393472 0 [35341401984]} 35341145680 0}] of type *string
     ^ accessed for the first time: use t17 as elem definition
   # *t17 = *&t16[t10]/syscall.Getenv.t17 (not found, type=string)
++ call builtin len(t18) # TODO (handle builtin)
   # t25 = t23 < t24
   # unhandled t19 = t18[t23]
   # t20 = t19 == 61:byte
   # t26 = t23 + 1:int
   # store *syscall.Getenv.t0 = syscall.Getenv.t27 of type string
   # store *syscall.Getenv.t1 = ???.true:bool of type bool
++ call (*sync.RWMutex).RUnlock()
-- return from (*sync.RWMutex).RUnlock (0 retvals)
   # *t0 = *local string (value) (not found)
   # *t1 = *local bool (found) (not found)
   # t30 = t23 + 1:int
   # store *syscall.Getenv.t0 = ???."":string of type string
   # store *syscall.Getenv.t1 = ???.false:bool of type bool
++ call (*sync.RWMutex).RUnlock()
-- return from (*sync.RWMutex).RUnlock (0 retvals)
   # *t0 = *local string (value) (not found)
   # *t1 = *local bool (found) (not found)
   # store *syscall.Getenv.t0 = ???."":string of type string
   # store *syscall.Getenv.t1 = ???.false:bool of type bool
++ call (*sync.RWMutex).RUnlock()
-- return from (*sync.RWMutex).RUnlock (0 retvals)
   # *t0 = *local string (value) (not found)
   # *t1 = *local bool (found) (not found)
-- return from syscall.Getenv (2 retvals)
   os.LookupEnv.t1 = extract t0[#0] == Undefined
   os.LookupEnv.t2 = extract t0[#1] == Undefined
-- return from os.LookupEnv (2 retvals)
   github.com/coreos/etcd/etcdmain.checkSupportArch.t1 = extract t0[#0] == Undefined
   github.com/coreos/etcd/etcdmain.checkSupportArch.t2 = extract t0[#1] == Undefined
   # t16 = t1 == "amd64":string
   github.com/coreos/etcd/etcdmain.checkSupportArch.t3 = *plog (global) of type **github.com/coreos/pkg/capnslog.PackageLogger
    ^ i.e. ???.plog@0
   # *plog = *github.com/coreos/etcd/etcdmain.plog/???.plog (not found, type=*github.com/coreos/pkg/capnslog.PackageLogger)
   github.com/coreos/etcd/etcdmain.checkSupportArch.t4 = Alloc (array@heap) of type *[1]interface{} (1 elems) at /Users/anthony/go/src/github.com/coreos/etcd/etcdmain/etcd.go:627:102
   github.com/coreos/etcd/etcdmain.checkSupportArch.t5 = &t4(=github.com/coreos/etcd/etcdmain.checkSupportArch.t4@0)[&{6393472 0}] of type *interface{}
     ^ accessed for the first time: use t5 as elem definition
   # github.com/coreos/etcd/etcdmain.checkSupportArch.t6 <- make interface{} <- string (t1)
   # store *github.com/coreos/etcd/etcdmain.checkSupportArch.t5 = github.com/coreos/etcd/etcdmain.checkSupportArch.t6 of type interface{}
++ call (*github.com/coreos/pkg/capnslog.PackageLogger).Warningf(p:caller[github.com/coreos/etcd/etcdmain.checkSupportArch.t3] = Undefined, format:caller[???."running etcd on u...":string] = Undefined, args:caller[github.com/coreos/etcd/etcdmain.checkSupportArch.t7] = Undefined)
++ call fmt.Sprintf()
-- Return from fmt.Sprintf (builtin/ext) with a single value
-- return from fmt.Sprintf (1 retvals)
   (*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t1 = Alloc (array@heap) of type *[1]interface{} (1 elems) at /Users/anthony/go/src/github.com/coreos/pkg/capnslog/pkg_logger.go:107:64
   (*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t2 = &t1(=(*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t1@0)[&{6393472 0}] of type *interface{}
     ^ accessed for the first time: use t2 as elem definition
   # (*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t3 <- make interface{} <- string (t0)
   # store *(*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t2 = (*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t3 of type interface{}
++ call (*github.com/coreos/pkg/capnslog.PackageLogger).internalLog(p:caller[(*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.p] = Undefined, depth:caller[???.2:int] = Undefined, inLevel:caller[???.1:github.com/coreos/pkg/capnslog.LogLevel] = Undefined, entries:caller[(*github.com/coreos/pkg/capnslog.PackageLogger).Warningf.t4] = Undefined)
[and so on]

Nil pointer dereference on ssa.RelString()

Hi! I'm playing around with your tool, it looks very promising.

I'm willing to participate in testing as there are packages that I'd like to have checked inside out, for instance github.com/zenhotels/astranet that is a custom multiplexer and it has a lot of high-grade concurrency logic inside.

So, running your tool results in a crash:

Net <- *multiplexer (t0) = (*github.com/zenhotels/astranet.multiplexer).copy.t0@2
-- return from (*github.com/zenhotels/astranet.multiplexer).Server (1 retvals)
panic: runtime error: invalid memory address or nil pointer dereference
[signal SIGSEGV: segmentation violation code=0x1 addr=0x58 pc=0x189097]

goroutine 691 [running]:
panic(0x5b6460, 0xc4200160b0)
    /usr/local/go/src/runtime/panic.go:500 +0x1a1
golang.org/x/tools/go/ssa.(*Function).RelString(0x0, 0x0, 0x626680, 0xc4252dfa80)
    /Users/xlab/Documents/dev/go/src/golang.org/x/tools/go/ssa/func.go:475 +0x37
golang.org/x/tools/go/ssa.(*Function).String(0x0, 0x0, 0xc42b778150)
    /Users/xlab/Documents/dev/go/src/golang.org/x/tools/go/ssa/ssa.go:1436 +0x34
github.com/nickng/dingo-hunter/cfsmextract.(*frame).callGo(0xc429badd80, 0xc42299cb90)
    /Users/xlab/Documents/dev/go/src/github.com/nickng/dingo-hunter/cfsmextract/func.go:302 +0x75b
github.com/nickng/dingo-hunter/cfsmextract.visitInst(0x8e3be0, 0xc42299cb90, 0xc429badd80)
    /Users/xlab/Documents/dev/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:70 +0x6d4
github.com/nickng/dingo-hunter/cfsmextract.visitBlock(0xc425420dc0, 0xc429badd80)
    /Users/xlab/Documents/dev/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:29 +0x94
github.com/nickng/dingo-hunter/cfsmextract.visitFunc(0xc4284e6140, 0xc429badd80, 0x658ed9)
    /Users/xlab/Documents/dev/go/src/github.com/nickng/dingo-hunter/cfsmextract/visit.go:41 +0x50
github.com/nickng/dingo-hunter/cfsmextract.(*CFSMExtract).Run(0xc4269a1bc0)
    /Users/xlab/Documents/dev/go/src/github.com/nickng/dingo-hunter/cfsmextract/cfsmextract.go:91 +0x625
created by github.com/nickng/dingo-hunter/cmd.extractCFSMs
    /Users/xlab/Documents/dev/go/src/github.com/nickng/dingo-hunter/cmd/cfsms.go:80 +0x587

I've got the latest golang.org/x/tools/go/ssa and Go 1.7.

README update

I ran dingo-hunter in CFSMs mode following README. The command ./runsmc.py inputs/deadlock_cfsms 2 was done but there is no SMC check in the terminal. Does README need to be updated？

Link to "Fencing off Go" is no longer valid

I would like to read this paper, but the link is no longer valid. Is there still a place where I can find a copy online?

golang/go/wiki/ResearchPapers

Hi!
this paper is removed from golang/go/wiki/ResearchPapers 😞

https://github.com/golang/go/wiki/ResearchPapers/_compare/fa4bab02ff787e6bb52ec71b43715afdd0a54948...7d15ba891fb30cb1c98dd1062b1853af937adb7c
history: https://github.com/golang/go/wiki/ResearchPapers/_history

Is it possible to re-add ? ( or revert changes ? )

Deadlock not detected in simple program

Dingo-Hunter is not able to detect a deadlock for the program below: (you can also find the code in this pastebin link https://pastebin.com/C4Md3yLB). The extracted CFSMs are correct, however the GMC synthesis succeeds for all 3 machines, when in fact it should fail.

This is the most simple example I am showing. I have other examples where deadlocks are not detected, when previously they were detected. Is it possible that an update in GMC synthesis tool caused deadlocks to go undetected ?

package main

type end struct{}

// !int . ?string . end
func party1(intChannel chan int, stringChannel chan string, endChannel chan end) {
	//!int
	intChannel <- 42
	// ?string
	<-stringChannel
	// end
	endChannel <- end{}

}

// !string . ?int . end
func party2(intChannel chan int, stringChannel chan string, endChannel chan end) {
	//!string
	stringChannel <- "Hello World"
	// ?int
	<-intChannel
	//end
	endChannel <- end{}
}

func main() {
	intChannel := make(chan int)
	stringChannel := make(chan string)
	endChannel := make(chan end)
	go party1(intChannel, stringChannel, endChannel)
	go party2(intChannel, stringChannel, endChannel)
	<-endChannel
	<-endChannel
}

go get failed

$  go get -u github.com/nickng/dingo-hunter
# github.com/nickng/dingo-hunter/cfsmextract/sesstype
src/github.com/nickng/dingo-hunter/cfsmextract/sesstype/dot.go:53: cannot use map[string]string literal (type map[string]string) as type gographviz.Attrs in field value
src/github.com/nickng/dingo-hunter/cfsmextract/sesstype/dot.go:65: cannot use map[string]string literal (type map[string]string) as type gographviz.Attrs in field value
src/github.com/nickng/dingo-hunter/cfsmextract/sesstype/dot.go:82: cannot use map[string]string literal (type map[string]string) as type gographviz.Attrs in field value
src/github.com/nickng/dingo-hunter/cfsmextract/sesstype/dot.go:99: cannot use map[string]string literal (type map[string]string) as type gographviz.Attrs in field value
src/github.com/nickng/dingo-hunter/cfsmextract/sesstype/dot.go:112: cannot use map[string]string literal (type map[string]string) as type gographviz.Attrs in field value
src/github.com/nickng/dingo-hunter/cfsmextract/sesstype/dot.go:132: cannot use dotNode.Attrs (type gographviz.Attrs) as type map[string]string in argument to dot.Graph.AddNode

golang.org/x/tools/go/ssa update causes build to fail

Recent update to golang/tools changes behaviour of CreateTestMainPackage (see golang/tools@8e53eb9) which now accepts only one ssa.Package instead of a slice. Call should be changed to use a for range loop instead.

The experimental nature of go/ssa needs a lot of maintenance. An option is to consider vendoring an old version of the ssa package.

Actions following the end of a branching get assigned to only one branch.

Actions after an internal choice or after an external choice (select-case) are assigned to one branch of each choice. (so there is no merge point after the choice).

For example, the file smallexample.go consists of a Sender goroutine that generates a random integer. If that integer is even it sends that integer through an int channel. If that integer is odd it sends a string through a string channel. Then it signals to main that it is done by sending a boolean to a bool channel.

!bool on the end channel (which is used to signal to main that a goroutine is exiting) is added to only one of the branches of the CFSMs (see output_cfsms_a_machines.svg, machines 4 and 5).