syncgraph

package
v0.0.0-...-3f344d0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Dec 19, 2021 License: GPL-2.0 Imports: 18 Imported by: 0

Documentation

Index

Constants

View Source 
const (
	WARNING_met_chan_var_buf = "WARNING_met_chan_var_buf"
	WARNING_met_nil_chan     = "WARNING_met_nil_chan"
)
View Source 
const Done = "Done"
View Source 
const EndDefer = 2
View Source 
const In_progress = "In_progress"
View Source 
const MaxRecursive = 1
View Source 
const NotInteresting = 0
View Source 
const (
	ZMode_GL = 0 // In this mode, only nodes of type *Go and SyncOp will be recorded
)

Variables

View Source 
var (
	Z3One  z3.Int
	Z3Zero z3.Int
)
View Source 
var DependMap map[interface{}]*DPrim
View Source 
var MapMeetCircularDependPrims map[interface{}]struct{}
View Source 
var PrintedBlockPosStr map[string]struct{} = make(map[string]struct{})

Functions

func EnumeratePathWithGoroutineHead 

func EnumeratePathWithGoroutineHead(head Node, enumeConfigure *EnumeConfigure) map[string]*LocalPath

Enumerate all possible paths of the given goroutine. If goroutine starts at function A, A has 3 paths, and in 2 paths A calls B, and B has 4 paths. Then we should return (1 + 2 * 4) paths, where B's path is inserted into A's path.

func GenDMap 

func GenDMap(vecChan []*instinfo.Channel, vecLocker []*instinfo.Locker) (DMap map[interface{}]*DPrim)

func TypeMsgForNode 

func TypeMsgForNode(node Node) string

func Walk 

func Walk(node Node, cfg *WalkConfig)

func WalkGenEdge 

func WalkGenEdge(node Node, mapHeadOfFn map[Node]bool)

Walk through node and its succs, to update node.In, node.Out and node.Num_Paths. Don't walk through backedge. Don't walk into callee, just append them to head_of_fn

Types

type AllConstraints 

type AllConstraints struct {
	Order         []z3.Bool
	SyncOfOp      []z3.Bool
	PairInferRule []z3.Bool
	Blocking      []z3.Bool
}

type Call 

type Call struct {
	Inst      ssa.CallInstruction
	Calling   map[*callgraph.Edge]Node
	NextLocal Node
	// contains filtered or unexported fields
}

func (*Call) CallCtx 

func (n *Call) CallCtx() *CallCtx

func (*Call) Context 

func (n *Call) Context() *CallCtx

func (*Call) GetId 

func (n *Call) GetId() int

func (*Call) GetString 

func (n *Call) GetString() string

func (*Call) In 

func (n *Call) In() []*NodeEdge

func (*Call) InAdd 

func (n *Call) InAdd(e *NodeEdge)

func (*Call) InOverWrite 

func (n *Call) InOverWrite(e *NodeEdge)

func (*Call) Instruction 

func (n *Call) Instruction() ssa.Instruction

func (*Call) Out 

func (n *Call) Out() []*NodeEdge

func (*Call) OutAdd 

func (n *Call) OutAdd(e *NodeEdge)

func (*Call) OutOverWrite 

func (n *Call) OutOverWrite(e *NodeEdge)

func (*Call) Parent 

func (n *Call) Parent() *SyncGraph

func (*Call) SetId 

func (n *Call) SetId(id int)

func (*Call) SetString 

func (n *Call) SetString(str string)

type CallCtx 

type CallCtx struct {
	CallChain *path.EdgeChain
	Goroutine *Goroutine
	CallSite  Node
	Graph     *SyncGraph
}

type ChainsToReachOp 

type ChainsToReachOp struct {
	Op                     interface{}
	Inst                   ssa.Instruction
	Chains                 []*path.EdgeChain
	VecBoolIsChainFinished []bool
	Finished               bool
}

Operation of a primitive, context-sensitive E.g. func send() { ch <- 1} 

func main() {
	send() // Line 3
	send() // Line 4
}

There are 2 operations, called by two paths: main() ---Line3---> send(); main() ---Line4---> send()

type ChanMake 

type ChanMake struct {
	Inst    *ssa.MakeChan
	Channel *instinfo.Channel
	MakeOp  instinfo.ChanOp
	Next    Node
	// contains filtered or unexported fields
}

func (*ChanMake) MapAliasOp 

func (a *ChanMake) MapAliasOp() map[SyncOp]bool

func (*ChanMake) MapSyncOp 

func (a *ChanMake) MapSyncOp() map[SyncOp]bool

func (*ChanMake) Operation 

func (c *ChanMake) Operation() interface{}

func (*ChanMake) Primitive 

func (a *ChanMake) Primitive() interface{}

type ChanOp 

type ChanOp struct {
	Channel *instinfo.Channel
	Op      instinfo.ChanOp
	Next    Node
	// contains filtered or unexported fields
}

Can be send/receive/close. Note that send and receive here must not be in select

func (*ChanOp) MapAliasOp 

func (a *ChanOp) MapAliasOp() map[SyncOp]bool

func (*ChanOp) MapSyncOp 

func (a *ChanOp) MapSyncOp() map[SyncOp]bool

func (*ChanOp) Operation 

func (a *ChanOp) Operation() interface{}

func (*ChanOp) Primitive 

func (a *ChanOp) Primitive() interface{}

type DEdge 

type DEdge struct {
	Caller *DPrim
	Callee *DPrim
}

type DPrim 

type DPrim struct {
	Primitive       interface{} // *instinfo.Channel or *instinfo.Locker
	Out             []*DEdge
	In              []*DEdge
	Circular_depend []*DPrim
	// contains filtered or unexported fields
}

func (*DPrim) AddCircularDepend 

func (prim *DPrim) AddCircularDepend(prim2 *DPrim)

func (*DPrim) AddOutEdge 

func (prim *DPrim) AddOutEdge(prim2 *DPrim)

func (*DPrim) IsCircularDepend 

func (prim *DPrim) IsCircularDepend(prim2 *DPrim) bool

type End 

type End struct {
	Inst   ssa.Instruction
	Reason int
	// contains filtered or unexported fields
}

func (*End) CallCtx 

func (n *End) CallCtx() *CallCtx

func (*End) Context 

func (n *End) Context() *CallCtx

func (*End) GetId 

func (n *End) GetId() int

func (*End) GetString 

func (n *End) GetString() string

func (*End) In 

func (n *End) In() []*NodeEdge

func (*End) InAdd 

func (n *End) InAdd(e *NodeEdge)

func (*End) InOverWrite 

func (n *End) InOverWrite(e *NodeEdge)

func (*End) Instruction 

func (n *End) Instruction() ssa.Instruction

func (*End) Out 

func (n *End) Out() []*NodeEdge

func (*End) OutAdd 

func (n *End) OutAdd(e *NodeEdge)

func (*End) OutOverWrite 

func (n *End) OutOverWrite(e *NodeEdge)

func (*End) Parent 

func (n *End) Parent() *SyncGraph

func (*End) SetId 

func (n *End) SetId(id int)

func (*End) SetString 

func (n *End) SetString(str string)

type EnumeConfigure 

type EnumeConfigure struct {
	Unfold             int
	IgnoreFn           map[*ssa.Function]struct{} // a map of not interesting
	FlagIgnoreNoSyncFn bool
	FlagIgnoreNormal   bool
}

type Go 

type Go struct {
	Inst                *ssa.Go
	MapCreateGoroutines map[*callgraph.Edge]*Goroutine
	MapCreateNodes      map[*callgraph.Edge]Node
	NextLocal           Node
	// contains filtered or unexported fields
}

func (*Go) CallCtx 

func (n *Go) CallCtx() *CallCtx

func (*Go) Context 

func (n *Go) Context() *CallCtx

func (*Go) GetId 

func (n *Go) GetId() int

func (*Go) GetString 

func (n *Go) GetString() string

func (*Go) In 

func (n *Go) In() []*NodeEdge

func (*Go) InAdd 

func (n *Go) InAdd(e *NodeEdge)

func (*Go) InOverWrite 

func (n *Go) InOverWrite(e *NodeEdge)

func (*Go) Instruction 

func (n *Go) Instruction() ssa.Instruction

func (*Go) Out 

func (n *Go) Out() []*NodeEdge

func (*Go) OutAdd 

func (n *Go) OutAdd(e *NodeEdge)

func (*Go) OutOverWrite 

func (n *Go) OutOverWrite(e *NodeEdge)

func (*Go) Parent 

func (n *Go) Parent() *SyncGraph

func (*Go) SetId 

func (n *Go) SetId(id int)

func (*Go) SetString 

func (n *Go) SetString(str string)

type Goroutine 

type Goroutine struct {
	Creator  *Go
	EntryFn  *ssa.Function
	IsMain   bool // If IsMain is true then Creator == nil
	HeadNode Node

	Graph *SyncGraph
}

type If 

type If struct {
	Inst               *ssa.If
	Cond               ssa.Value
	Then               Node
	Else               Node
	BoolIsThenBackedge bool
	BoolIsElseBackedge bool
	// contains filtered or unexported fields
}

func (*If) CallCtx 

func (n *If) CallCtx() *CallCtx

func (*If) Context 

func (n *If) Context() *CallCtx

func (*If) GetId 

func (n *If) GetId() int

func (*If) GetString 

func (n *If) GetString() string

func (*If) In 

func (n *If) In() []*NodeEdge

func (*If) InAdd 

func (n *If) InAdd(e *NodeEdge)

func (*If) InOverWrite 

func (n *If) InOverWrite(e *NodeEdge)

func (*If) Instruction 

func (n *If) Instruction() ssa.Instruction

func (*If) Out 

func (n *If) Out() []*NodeEdge

func (*If) OutAdd 

func (n *If) OutAdd(e *NodeEdge)

func (*If) OutOverWrite 

func (n *If) OutOverWrite(e *NodeEdge)

func (*If) Parent 

func (n *If) Parent() *SyncGraph

func (*If) SetId 

func (n *If) SetId(id int)

func (*If) SetString 

func (n *If) SetString(str string)

type InstCtxKey 

type InstCtxKey struct {
	Inst ssa.Instruction
	Ctx  *CallCtx
}

type Jump 

type Jump struct {
	Inst            *ssa.Jump
	Next            Node
	BoolIsNextexist bool
	BoolIsBackedge  bool
	// contains filtered or unexported fields
}

func (*Jump) CallCtx 

func (n *Jump) CallCtx() *CallCtx

func (*Jump) Context 

func (n *Jump) Context() *CallCtx

func (*Jump) GetId 

func (n *Jump) GetId() int

func (*Jump) GetString 

func (n *Jump) GetString() string

func (*Jump) In 

func (n *Jump) In() []*NodeEdge

func (*Jump) InAdd 

func (n *Jump) InAdd(e *NodeEdge)

func (*Jump) InOverWrite 

func (n *Jump) InOverWrite(e *NodeEdge)

func (*Jump) Instruction 

func (n *Jump) Instruction() ssa.Instruction

func (*Jump) Out 

func (n *Jump) Out() []*NodeEdge

func (*Jump) OutAdd 

func (n *Jump) OutAdd(e *NodeEdge)

func (*Jump) OutOverWrite 

func (n *Jump) OutOverWrite(e *NodeEdge)

func (*Jump) Parent 

func (n *Jump) Parent() *SyncGraph

func (*Jump) SetId 

func (n *Jump) SetId(id int)

func (*Jump) SetString 

func (n *Jump) SetString(str string)

type Kill 

type Kill struct {
	Inst        ssa.Instruction // can be *ssa.Panic or *ssa.Call (callee is t.Fatal/Fatalf/...)
	BoolIsPanic bool
	BoolIsFatal bool
	Next        Node
	// contains filtered or unexported fields
}

func (*Kill) CallCtx 

func (n *Kill) CallCtx() *CallCtx

func (*Kill) Context 

func (n *Kill) Context() *CallCtx

func (*Kill) GetId 

func (n *Kill) GetId() int

func (*Kill) GetString 

func (n *Kill) GetString() string

func (*Kill) In 

func (n *Kill) In() []*NodeEdge

func (*Kill) InAdd 

func (n *Kill) InAdd(e *NodeEdge)

func (*Kill) InOverWrite 

func (n *Kill) InOverWrite(e *NodeEdge)

func (*Kill) Instruction 

func (n *Kill) Instruction() ssa.Instruction

func (*Kill) Out 

func (n *Kill) Out() []*NodeEdge

func (*Kill) OutAdd 

func (n *Kill) OutAdd(e *NodeEdge)

func (*Kill) OutOverWrite 

func (n *Kill) OutOverWrite(e *NodeEdge)

func (*Kill) Parent 

func (n *Kill) Parent() *SyncGraph

func (*Kill) SetId 

func (n *Kill) SetId(id int)

func (*Kill) SetString 

func (n *Kill) SetString(str string)

type LocalPath 

type LocalPath struct {
	Path []Node
	Hash string
	// contains filtered or unexported fields
}

func NewEmptyPath 

func NewEmptyPath() *LocalPath

func (*LocalPath) IsEmpty 

func (l *LocalPath) IsEmpty() bool

type LockerOp 

type LockerOp struct {
	Locker *instinfo.Locker
	Op     instinfo.LockerOp
	Next   Node
	// contains filtered or unexported fields
}

func (*LockerOp) MapAliasOp 

func (a *LockerOp) MapAliasOp() map[SyncOp]bool

func (*LockerOp) MapSyncOp 

func (a *LockerOp) MapSyncOp() map[SyncOp]bool

func (*LockerOp) Operation 

func (a *LockerOp) Operation() interface{}

func (*LockerOp) Primitive 

func (a *LockerOp) Primitive() interface{}

type Node 

type Node interface {
	Context() *CallCtx
	Instruction() ssa.Instruction
	Parent() *SyncGraph
	In() []*NodeEdge
	Out() []*NodeEdge
	CallCtx() *CallCtx
	InAdd(*NodeEdge)
	OutAdd(*NodeEdge)
	InOverWrite(*NodeEdge)
	OutOverWrite(*NodeEdge)
	SetId(int)
	GetId() int
	SetString(string)
	GetString() string
}

func Fake_Node 

func Fake_Node() Node

Returns a unique Node that doesn't have any information

func ProcessInstGetNode 

func ProcessInstGetNode(targetInst ssa.Instruction, ctx *CallCtx) Node

type NodeEdge 

type NodeEdge struct {
	Prev       Node
	Succ       Node
	IsBackedge bool
	IsCall     bool
	IsGo       bool
	AddValue   int
}

type NormalInst 

type NormalInst struct {
	Inst ssa.Instruction
	Next Node
	// contains filtered or unexported fields
}

func (*NormalInst) CallCtx 

func (n *NormalInst) CallCtx() *CallCtx

func (*NormalInst) Context 

func (n *NormalInst) Context() *CallCtx

func (*NormalInst) GetId 

func (n *NormalInst) GetId() int

func (*NormalInst) GetString 

func (n *NormalInst) GetString() string

func (*NormalInst) In 

func (n *NormalInst) In() []*NodeEdge

func (*NormalInst) InAdd 

func (n *NormalInst) InAdd(e *NodeEdge)

func (*NormalInst) InOverWrite 

func (n *NormalInst) InOverWrite(e *NodeEdge)

func (*NormalInst) Instruction 

func (n *NormalInst) Instruction() ssa.Instruction

func (*NormalInst) Out 

func (n *NormalInst) Out() []*NodeEdge

func (*NormalInst) OutAdd 

func (n *NormalInst) OutAdd(e *NodeEdge)

func (*NormalInst) OutOverWrite 

func (n *NormalInst) OutOverWrite(e *NodeEdge)

func (*NormalInst) Parent 

func (n *NormalInst) Parent() *SyncGraph

func (*NormalInst) SetId 

func (n *NormalInst) SetId(id int)

func (*NormalInst) SetString 

func (n *NormalInst) SetString(str string)

type Overwrite 

type Overwrite struct {
	Inst *ssa.MakeChan
	Chan *instinfo.Channel
	// contains filtered or unexported fields
}

func (*Overwrite) CallCtx 

func (n *Overwrite) CallCtx() *CallCtx

func (*Overwrite) Context 

func (n *Overwrite) Context() *CallCtx

func (*Overwrite) GetId 

func (n *Overwrite) GetId() int

func (*Overwrite) GetString 

func (n *Overwrite) GetString() string

func (*Overwrite) In 

func (n *Overwrite) In() []*NodeEdge

func (*Overwrite) InAdd 

func (n *Overwrite) InAdd(e *NodeEdge)

func (*Overwrite) InOverWrite 

func (n *Overwrite) InOverWrite(e *NodeEdge)

func (*Overwrite) Instruction 

func (n *Overwrite) Instruction() ssa.Instruction

func (*Overwrite) Out 

func (n *Overwrite) Out() []*NodeEdge

func (*Overwrite) OutAdd 

func (n *Overwrite) OutAdd(e *NodeEdge)

func (*Overwrite) OutOverWrite 

func (n *Overwrite) OutOverWrite(e *NodeEdge)

func (*Overwrite) Parent 

func (n *Overwrite) Parent() *SyncGraph

func (*Overwrite) SetId 

func (n *Overwrite) SetId(id int)

func (*Overwrite) SetString 

func (n *Overwrite) SetString(str string)

type PNode 

type PNode struct {
	Path     *LocalPath
	Index    int
	Node     Node
	Blocked  bool
	Executed bool
}

type PPath 

type PPath struct {
	Path []*PNode
	// contains filtered or unexported fields
}

func (PPath) IsNodeIn 

func (p PPath) IsNodeIn(node Node) bool

func (*PPath) PrintPPath 

func (p *PPath) PrintPPath()

func (PPath) SetAllReached 

func (p PPath) SetAllReached()

func (PPath) SetBlockAt 

func (p PPath) SetBlockAt(index int)

type Return 

type Return struct {
	Inst                 ssa.Instruction
	BoolIsEndOfGoroutine bool
	Caller               Node
	// contains filtered or unexported fields
}

func (*Return) CallCtx 

func (n *Return) CallCtx() *CallCtx

func (*Return) Context 

func (n *Return) Context() *CallCtx

func (*Return) GetId 

func (n *Return) GetId() int

func (*Return) GetString 

func (n *Return) GetString() string

func (*Return) In 

func (n *Return) In() []*NodeEdge

func (*Return) InAdd 

func (n *Return) InAdd(e *NodeEdge)

func (*Return) InOverWrite 

func (n *Return) InOverWrite(e *NodeEdge)

func (*Return) Instruction 

func (n *Return) Instruction() ssa.Instruction

func (*Return) Out 

func (n *Return) Out() []*NodeEdge

func (*Return) OutAdd 

func (n *Return) OutAdd(e *NodeEdge)

func (*Return) OutOverWrite 

func (n *Return) OutOverWrite(e *NodeEdge)

func (*Return) Parent 

func (n *Return) Parent() *SyncGraph

func (*Return) SetId 

func (n *Return) SetId(id int)

func (*Return) SetString 

func (n *Return) SetString(str string)

type Select 

type Select struct {
	Inst           *ssa.Select
	Cases          map[int]*SelectCase
	BoolHasDefault bool
	DefaultCase    *SelectCase
	// contains filtered or unexported fields
}

func (*Select) CallCtx 

func (n *Select) CallCtx() *CallCtx

func (*Select) Context 

func (n *Select) Context() *CallCtx

func (*Select) GetId 

func (n *Select) GetId() int

func (*Select) GetString 

func (n *Select) GetString() string

func (*Select) In 

func (n *Select) In() []*NodeEdge

func (*Select) InAdd 

func (n *Select) InAdd(e *NodeEdge)

func (*Select) InOverWrite 

func (n *Select) InOverWrite(e *NodeEdge)

func (*Select) Instruction 

func (n *Select) Instruction() ssa.Instruction

func (*Select) Out 

func (n *Select) Out() []*NodeEdge

func (*Select) OutAdd 

func (n *Select) OutAdd(e *NodeEdge)

func (*Select) OutOverWrite 

func (n *Select) OutOverWrite(e *NodeEdge)

func (*Select) Parent 

func (n *Select) Parent() *SyncGraph

func (*Select) SetId 

func (n *Select) SetId(id int)

func (*Select) SetString 

func (n *Select) SetString(str string)

type SelectCase 

type SelectCase struct {
	Channel        *instinfo.Channel
	Op             instinfo.ChanOp
	Index          int // -1 if this is default
	BoolIsDefault  bool
	Next           Node
	BoolIsBackedge bool
	Select         *Select
	// contains filtered or unexported fields
}

func (*SelectCase) MapAliasOp 

func (a *SelectCase) MapAliasOp() map[SyncOp]bool

func (*SelectCase) MapSyncOp 

func (a *SelectCase) MapSyncOp() map[SyncOp]bool

func (*SelectCase) Operation 

func (a *SelectCase) Operation() interface{}

func (*SelectCase) Primitive 

func (a *SelectCase) Primitive() interface{}

type Status 

type Status struct {
	Str     string // Str can be In_progress or Done. Only used to decide backedge for local nodes
	Visited int
}

type SyncGraph 

type SyncGraph struct {
	// Prepare
	MainGoroutine    *Goroutine   // MainGoroutine is the Goroutine that is both a head and it contains the MakeChan operation
	HeadGoroutines   []*Goroutine // HeadGoroutines are the starting Goroutines that don't have creator in the graph
	Goroutines       []*Goroutine
	MapFirstNodeOfFn map[Node]struct{} // All Nodes that are the first Node of a function in SyncGraph
	Task             *Task

	// Build
	MapInstCtxKey2Node  map[InstCtxKey]Node // Two kinds of Node is not in this map: SelectCase, rundefer's Nodes
	Select2Case         map[*Select][]*SelectCase
	MapInstCtxKey2Defer map[InstCtxKey][]Node
	NodeStatus          map[Node]*Status
	MapPrim2VecSyncOp   map[interface{}][]SyncOp
	Visited             []*path.EdgeChain
	Worklist            []*Unfinish
	MapFnOnOpPath       map[*ssa.Function]struct{} // a map of functions that are on a path to reach a sync operation

	// Enumerate path
	PathCombinations []*pathCombination
	EnumerateCfg     *EnumeConfigure
}

func BuildGraph 

func BuildGraph(ch *instinfo.Channel, vecChannel []*instinfo.Channel, vecLocker []*instinfo.Locker, DMap map[interface{}]*DPrim) (*SyncGraph, error)

func NewGraph 

func NewGraph(task *Task) *SyncGraph

func (*SyncGraph) BuildNodeInOut 

func (g *SyncGraph) BuildNodeInOut()

This function updates Node.Num_paths and NodeEdge.AddValue

func (SyncGraph) CheckWithZ3 

func (g SyncGraph) CheckWithZ3() bool

func (*SyncGraph) ComputeFnOnOpPath 

func (g *SyncGraph) ComputeFnOnOpPath()

Update g.MapFnOnOpPath.

func (*SyncGraph) EnumerateAllPathCombinations 

func (g *SyncGraph) EnumerateAllPathCombinations()

Enumerate all path combinations. A pathCombination: a slice of {one goroutine and one path}. Path can be Not_execute, meaning empty path. Note that the number of goroutine_path may be greater than len(g.Goroutines). For example, if a *Go is visited 3 times, we create 3 goroutines

func (*SyncGraph) NewCtx 

func (g *SyncGraph) NewCtx(goroutine *Goroutine, head *ssa.Function) *CallCtx

func (*SyncGraph) NewGoroutine 

func (g *SyncGraph) NewGoroutine(headFn *ssa.Function) *Goroutine

func (*SyncGraph) OptimizeBB_V1 

func (g *SyncGraph) OptimizeBB_V1()

If BB X post-dominates BB Y, and all BBs on any path from Y to X don't contain important Nodes, and X and Y are in the same layer of loop, we can ignore these BBs between X and Y. We will link Y and X directly (let the first Node of X be the next Node of the last Node of Y) What are important Nodes: Call to functions on MapFnOnOpPath/ operation of dependent primitives/ Return/ Kill/ End

func (*SyncGraph) OptimizeBB_V2 

func (g *SyncGraph) OptimizeBB_V2()

func (*SyncGraph) PrintAllPathCombinations 

func (g *SyncGraph) PrintAllPathCombinations()

func (*SyncGraph) PrintGraphAllNodesType 

func (g *SyncGraph) PrintGraphAllNodesType()

Walk the whole graph, print type of node on path

func (*SyncGraph) SetEnumCfg 

func (g *SyncGraph) SetEnumCfg(unfold int, flagIgnoreNoSyncFn bool, flagIgnoreNormal bool)

type SyncOp 

type SyncOp interface {
	Primitive() interface{} // *channel.Channel or *locker.Locker or *cond.Cond or *waitgroup.WG
	MapAliasOp() map[SyncOp]bool
	MapSyncOp() map[SyncOp]bool
	Operation() interface{}
}

type Task 

type Task struct {
	VecTaskPrimitive                []*TaskPrimitive // VecTaskPrimitive means these primitives satify: all its operations are in the graph
	MapValue2TaskPrimitive          map[interface{}]*TaskPrimitive
	MapLCARoot2Op                   map[*ssa.Function][]*ChainsToReachOp
	BoolFinished                    bool
	BoolGiveupIfCallgraphInaccurate bool
}

func (*Task) IsPrimATarget 

func (t *Task) IsPrimATarget(prim interface{}) bool

A primitive is a target when it is in Task.VecTaskPrimitive

func (*Task) Step1AddPrim 

func (t *Task) Step1AddPrim(newP interface{})

After this function, a new primitive is added to the task, but TaskPrimitive.Ops are not completed. Need to run Step2CompletePrims after adding all primitives

func (*Task) Step2CompletePrims 

func (t *Task) Step2CompletePrims() error

After adding all primitives that we want, complete everything in each TaskPrimitive.Ops

func (*Task) Update 

func (t *Task) Update()

func (*Task) WantedList 

func (t *Task) WantedList() (result []*path.EdgeChain)

type TaskPrimitive 

type TaskPrimitive struct {
	Primitive interface{}
	Ops       map[interface{}]*ChainsToReachOp
	Finished  bool
	Task      *Task
}

func (*TaskPrimitive) CompleteOps 

func (tp *TaskPrimitive) CompleteOps(LCA2paths map[*ssa.Function][]*path.EdgeChain)

Generates tp.Ops, and find all callchains from head to an operation

type TupleAPIFunc 

type TupleAPIFunc struct {
	PkgName  string
	FuncName string
}

type Unfinish 

type Unfinish struct {
	UnfinishedFn *ssa.Function
	Unfinished   Node
	IsGo         bool
	Site         *callgraph.Edge // Site.Callee has at least 1 bb, and this bb has at least 1 inst
	Dir          bool            // true if Call/Go (from caller to callee), false if Return (from callee to caller)
	Ctx          *CallCtx        // a new CallCtx used for the Site. This can be directly used
}

type WalkConfig 

type WalkConfig struct {
	NoBackedge bool
	NoCallee   bool
	EntryFn    func(Node)
	EdgeFn     func(*NodeEdge) // called when meet an edge, before deciding whether to skip edge according to NoBackedge or NoCallee
	ExitFn     func(Node)
}

type Z3Cfg 

type Z3Cfg struct {
	Mode int
}

type Z3System 

type Z3System struct {
	Constraints *AllConstraints

	Warnings []string
	Config   *Z3Cfg
	Z3Ctx    *z3.Context
	Solver   *z3.Solver
	// contains filtered or unexported fields
}

func NewZ3ForGl 

func NewZ3ForGl() *Z3System

func (*Z3System) Assert 

func (z *Z3System) Assert()

Assert puts assertions stored in z.Contraints into the solver

func (*Z3System) Prepare 

func (z *Z3System) Prepare(vecPPath []*PPath, vecBlockPos []blockingPos) error

Initialize z.vecZGoroutines; generate ZNodes on each ZGoroutine from p_paths; generate constraints

func (*Z3System) PrintAssert 

func (z *Z3System) PrintAssert()

func (*Z3System) Z3Main 

func (z *Z3System) Z3Main(p_paths []*PPath, block_poses []blockingPos) bool

type ZGoroutine 

type ZGoroutine struct {
	PtrPPath     *PPath
	Nodes        []ZNode // Not all nodes in PPath will be reserved
	IsTerminated bool
	BlockAt      int
	ID           int

	Z3Sys *Z3System
}

type ZNode 

type ZNode interface {
	ID() int
	SetId(int)
	Goroutine() *ZGoroutine
	PNode() *PNode
	IsBlocking() bool
	TraceOrder() z3.Int
	UpdateOrder(z3.Int)
}

type ZNodeBRecv 

type ZNodeBRecv struct {
	Buffer     z3.Int
	Other_SR   []ZNode
	Closes     []*ZNodeClose
	From_close z3.Bool
	IsUnlock   bool
	ZNodeBasic
}

type ZNodeBSend 

type ZNodeBSend struct {
	Buffer   z3.Int
	Other_SR []ZNode
	IsLock   bool
	ZNodeBasic
}

type ZNodeBasic 

type ZNodeBasic struct {
	Id         int
	ZGoroutine *ZGoroutine
	PtrPNode   *PNode

	Order z3.Int
	// contains filtered or unexported fields
}

func (*ZNodeBasic) Goroutine 

func (b *ZNodeBasic) Goroutine() *ZGoroutine

func (*ZNodeBasic) ID 

func (b *ZNodeBasic) ID() int

func (*ZNodeBasic) IsBlocking 

func (b *ZNodeBasic) IsBlocking() bool

func (*ZNodeBasic) PNode 

func (b *ZNodeBasic) PNode() *PNode

func (*ZNodeBasic) SetId 

func (b *ZNodeBasic) SetId(id int)

func (*ZNodeBasic) TraceOrder 

func (b *ZNodeBasic) TraceOrder() z3.Int

func (*ZNodeBasic) UpdateOrder 

func (b *ZNodeBasic) UpdateOrder(i z3.Int)

type ZNodeClose 

type ZNodeClose struct {
	ZNodeBasic
}

type ZNodeNbRecv 

type ZNodeNbRecv struct {
	ZNodeBasic
	Pairs     []*ZSendRecvPair
	Closes    []*ZNodeClose
	FromClose z3.Bool
}

type ZNodeNbSend 

type ZNodeNbSend struct {
	ZNodeBasic
	Closes []*ZNodeClose
	Pairs  []*ZSendRecvPair
}

type ZSendRecvPair 

type ZSendRecvPair struct {
	Send *ZNodeNbSend
	Recv *ZNodeNbRecv
	// contains filtered or unexported fields
}

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.