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
}

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL