Documentation ¶
Index ¶
- Constants
- Variables
- func ConfigAI(c AIConfig) prepAI
- func Create() factory
- func PrepareAI() prepAI
- func StringifyNodeArguments(g defs.Goro, mem L.Memory, node cfg.Node) (label string)
- func VisualizeIntraprocess(g defs.Goro, edges map[defs.CtrLoc][]defs.CtrLoc, ...)
- type ABSTRACTION_LEVEL
- type AIConfig
- type AbsConfiguration
- func (s *AbsConfiguration) Abstract(abstractTo ABSTRACTION_LEVEL) Configuration
- func (s *AbsConfiguration) AbstractionLevel() ABSTRACTION_LEVEL
- func (s *AbsConfiguration) AddPredecessor(s1 *AbsConfiguration)
- func (s *AbsConfiguration) Copy() *AbsConfiguration
- func (s *AbsConfiguration) Derive(threads map[defs.Goro]defs.CtrLoc) *AbsConfiguration
- func (s *AbsConfiguration) DeriveThread(tid defs.Goro, cl defs.CtrLoc) *AbsConfiguration
- func (s *AbsConfiguration) ForEach(do func(defs.Goro, defs.CtrLoc))
- func (s *AbsConfiguration) Get(g defs.Goro) (defs.CtrLoc, bool)
- func (s *AbsConfiguration) GetCommSuccessors(leaves map[defs.Goro]map[defs.CtrLoc]struct{}, state L.AnalysisState) (S transfers)
- func (s *AbsConfiguration) GetSilentSuccessors(C AnalysisCtxt, g defs.Goro, initState L.AnalysisState) transfers
- func (s *AbsConfiguration) GetTransitions(C AnalysisCtxt, initState L.AnalysisState) transfers
- func (s *AbsConfiguration) GetUnsafe(g defs.Goro) defs.CtrLoc
- func (s *AbsConfiguration) Hash() uint32
- func (s *AbsConfiguration) Init(abs ABSTRACTION_LEVEL) Configuration
- func (s *AbsConfiguration) IsPanicked() bool
- func (s *AbsConfiguration) IsSynchronizing(C AnalysisCtxt, state L.AnalysisState) bool
- func (s *AbsConfiguration) Main() defs.Goro
- func (s0 *AbsConfiguration) OldVisualize()
- func (s *AbsConfiguration) PrettyPrint()
- func (s *AbsConfiguration) SetThreads(threads defs.Superloc)
- func (s *AbsConfiguration) String() string
- func (s *AbsConfiguration) Superlocation() defs.Superloc
- func (s *AbsConfiguration) Threads() defs.Superloc
- func (s0 *AbsConfiguration) Visualize()
- type AbsCtrlLoc
- type AnalysisCtxt
- func (C AnalysisCtxt) Blacklisted(callIns ssa.CallInstruction, sfun *ssa.Function) bool
- func (C AnalysisCtxt) CheckMaxSuperloc(s defs.Superloc, spawnee defs.Goro)
- func (C AnalysisCtxt) CheckMemory(m L.Memory)
- func (C AnalysisCtxt) CheckPointsTo(v L.PointsTo)
- func (C *AnalysisCtxt) FragmentPredicateFromPrimitives(primitives []ssa.Value, ...)
- func (C AnalysisCtxt) IsPrimitiveFocused(prim ssa.Value) bool
- func (C AnalysisCtxt) LogCtrLocMemory(g defs.Goro, cl defs.CtrLoc, m L.Memory)
- func (C AnalysisCtxt) LogSuperlocation(sl defs.Superloc)
- func (C *AnalysisCtxt) LogWildcardSwap(m L.Memory, l loc.Location)
- func (C AnalysisCtxt) TopInjectParams(callIns ssa.CallInstruction, g defs.Goro, state L.AnalysisState, ...) L.Memory
- type BaseConfiguration
- type Blocks
- func (o Blocks) Exists(pred func(sl defs.Superloc, gs map[defs.Goro]struct{}) bool) bool
- func (o Blocks) Find(pred func(sl defs.Superloc, gs map[defs.Goro]struct{}) bool) (defs.Superloc, map[defs.Goro]struct{}, bool)
- func (o Blocks) ForEach(do func(sl defs.Superloc, gs map[defs.Goro]struct{}))
- func (o Blocks) Log()
- func (o Blocks) PrintPath(G SuperlocGraph, A L.Analysis, g graph.Graph[*ssa.Function])
- func (o Blocks) String() string
- func (o Blocks) UpdateWith(other Blocks)
- type Configuration
- type ConfigurationSuccessors
- type FragmentPredicate
- type Metrics
- func (m *Metrics) AddCallees(callIns ssa.CallInstruction, calleeSet funset)
- func (m *Metrics) AddChan(cl defs.CtrLoc)
- func (m *Metrics) AddCommOp(cl defs.CtrLoc)
- func (m *Metrics) AddGo(cl defs.CtrLoc)
- func (m *Metrics) Blocks() Blocks
- func (m *Metrics) CallsiteCallees() map[ssa.CallInstruction]funset
- func (m *Metrics) Chans() map[ssa.Instruction]struct{}
- func (m *Metrics) ConcurrencyOps() map[ssa.Instruction]struct{}
- func (m *Metrics) Done()
- func (m *Metrics) Enabled() bool
- func (m *Metrics) Error() string
- func (m *Metrics) ExpandFunction(f *ssa.Function)
- func (m *Metrics) Functions() map[*ssa.Function]int
- func (m *Metrics) Gos() map[ssa.Instruction]struct{}
- func (m *Metrics) HasConcurrency() bool
- func (m *Metrics) IsRelevant() bool
- func (m *Metrics) MaxCallees() (ins ssa.CallInstruction, max int)
- func (m *Metrics) Panic(err interface{})
- func (m *Metrics) Performance() string
- func (m *Metrics) SetBlocks(blocks Blocks)
- func (m *Metrics) Skip()
- func (m *Metrics) TimerStart()
- type Successor
- type SuperlocGraph
- func (G SuperlocGraph) Entry() *AbsConfiguration
- func (G SuperlocGraph) ForEach(do func(*AbsConfiguration))
- func (G SuperlocGraph) Get(s *AbsConfiguration) *AbsConfiguration
- func (G SuperlocGraph) PrettyPrint()
- func (G SuperlocGraph) Size() int
- func (G SuperlocGraph) String() (str string)
- func (G SuperlocGraph) Terminals() map[*AbsConfiguration]struct{}
- func (G SuperlocGraph) ToGraph() graph.Graph[*AbsConfiguration]
Constants ¶
const ( // "May" mode overapproximates the possiblity of a blocked goroutine. // This mode will register a potential orphan if any path might lead to orphanage. MAY = iota // "Must" mode underapproximates the possibility of a blocked goroutine. // In this mode, potential blocks are not considered if they have at least // one "non-orphaning" future. If all futures point to orphanage, MUST )
Blocked goroutine analysis mode
const ( ABS_CONCRETE = iota ABS_BUFFER ABS_COARSE )
Variables ¶
var ( Lattices = L.Create().Lattice Elements = L.Create().Element )
var ( OUTCOME_BUGS_FOUND = "Bugs found" OUTCOME_NO_BUGS_FOUND = "No bugs found" OUTCOME_PANIC = "Panicked" OUTCOME_SKIP = "Skipped" )
var ErrFocusedPrimitiveSwapped = errors.New("Focused primitive was wildcard swapped")
var ErrUnboundedGoroutineSpawn = errors.New("Unbounded goroutine spawns detected")
var EvaluateSSA = evaluateSSA
TODO: Should probably just change all occurences of evaluateSSA to EvaluateSSA instead
Functions ¶
func ConfigAI ¶
func ConfigAI(c AIConfig) prepAI
Prepare Abstract Interpretation based on a configuration (e. g. collect metrics)
func PrepareAI ¶
func PrepareAI() prepAI
Interface to prepare abstract interpretation. Depending on preparation, generates a different analysis context
func StringifyNodeArguments ¶
func VisualizeIntraprocess ¶
func VisualizeIntraprocess( g defs.Goro, edges map[defs.CtrLoc][]defs.CtrLoc, analysis map[defs.CtrLoc]L.AnalysisState, )
Debugging utility I made to visualize results of intraprocedural abstract interpretation If -verbose is specified the SSA-nodes will be annotated with abstract values for operands.
Types ¶
type ABSTRACTION_LEVEL ¶
type ABSTRACTION_LEVEL int
func (ABSTRACTION_LEVEL) String ¶
func (a ABSTRACTION_LEVEL) String() string
type AbsConfiguration ¶
type AbsConfiguration struct { BaseConfiguration Target defs.Goro // contains filtered or unexported fields }
An abstract configuration involves a super location, (optionally) bookkeeping of the targeted thread, and other path conditions, e. g. channel status in terms of closing.
func CoarseProgress ¶
func CoarseProgress(C AnalysisCtxt) ( *AbsConfiguration, L.AnalysisState, )
Takes an abstract configuration and tries to progress threads as far as possible using only silent transitions. If a goroutine can end up in multiple places it is not progressed further.
func (*AbsConfiguration) Abstract ¶
func (s *AbsConfiguration) Abstract(abstractTo ABSTRACTION_LEVEL) Configuration
Coarse configuration cannot be abstracted further. Acts as the identity function if given the coarse abstraction level.
func (*AbsConfiguration) AbstractionLevel ¶
func (s *AbsConfiguration) AbstractionLevel() ABSTRACTION_LEVEL
func (*AbsConfiguration) AddPredecessor ¶
func (s *AbsConfiguration) AddPredecessor(s1 *AbsConfiguration)
func (*AbsConfiguration) Copy ¶
func (s *AbsConfiguration) Copy() *AbsConfiguration
Create deep copy of configurations
func (*AbsConfiguration) Derive ¶
func (s *AbsConfiguration) Derive(threads map[defs.Goro]defs.CtrLoc) *AbsConfiguration
Derive new superlocation for given configuration.
func (*AbsConfiguration) DeriveThread ¶
func (s *AbsConfiguration) DeriveThread(tid defs.Goro, cl defs.CtrLoc) *AbsConfiguration
func (*AbsConfiguration) ForEach ¶
func (s *AbsConfiguration) ForEach(do func(defs.Goro, defs.CtrLoc))
func (*AbsConfiguration) GetCommSuccessors ¶
func (s *AbsConfiguration) GetCommSuccessors( leaves map[defs.Goro]map[defs.CtrLoc]struct{}, state L.AnalysisState, ) (S transfers)
func (*AbsConfiguration) GetSilentSuccessors ¶
func (s *AbsConfiguration) GetSilentSuccessors( C AnalysisCtxt, g defs.Goro, initState L.AnalysisState, ) transfers
Returns possible multi-step silent successors for the given thread. Uses the abstract interpretation framework to model the effects of single steps on the way. (This method contains an internal fixpoint computation.)
func (*AbsConfiguration) GetTransitions ¶
func (s *AbsConfiguration) GetTransitions( C AnalysisCtxt, initState L.AnalysisState) transfers
func (*AbsConfiguration) Hash ¶
func (s *AbsConfiguration) Hash() uint32
func (*AbsConfiguration) Init ¶
func (s *AbsConfiguration) Init(abs ABSTRACTION_LEVEL) Configuration
func (*AbsConfiguration) IsPanicked ¶
func (s *AbsConfiguration) IsPanicked() bool
Returns true iff. the configuration contains a panicked goroutine
func (*AbsConfiguration) IsSynchronizing ¶
func (s *AbsConfiguration) IsSynchronizing(C AnalysisCtxt, state L.AnalysisState) bool
func (*AbsConfiguration) Main ¶
func (s *AbsConfiguration) Main() defs.Goro
func (*AbsConfiguration) OldVisualize ¶
func (s0 *AbsConfiguration) OldVisualize()
Construct a Dot graph given a starting coarse configuration.
func (*AbsConfiguration) PrettyPrint ¶
func (s *AbsConfiguration) PrettyPrint()
func (*AbsConfiguration) SetThreads ¶
func (s *AbsConfiguration) SetThreads(threads defs.Superloc)
Statefully set the threads in the given configuration. Usage recommended only on expendable deep copies of configurations.
func (*AbsConfiguration) String ¶
func (s *AbsConfiguration) String() string
func (*AbsConfiguration) Superlocation ¶
func (s *AbsConfiguration) Superlocation() defs.Superloc
func (*AbsConfiguration) Threads ¶
func (s *AbsConfiguration) Threads() defs.Superloc
func (*AbsConfiguration) Visualize ¶
func (s0 *AbsConfiguration) Visualize()
Construct a Dot graph given a starting coarse configuration.
type AbsCtrlLoc ¶
An abstract thread involves a CFG node and a root function indicating the function that was called when spawning the goroutine. Upon exiting the root function, a possible successor would be the termination of the goroutine. Together, they form an abstract control location.
type AnalysisCtxt ¶
type AnalysisCtxt struct { Function *ssa.Function LoadRes tu.LoadResult InitConf *AbsConfiguration InitState L.AnalysisState // Determines which functions to "expand", essentially defining the // fragment of the program to analyze. FragmentPredicate FragmentPredicate // Akin to "PSet" in GCatch FocusedPrimitives []ssa.Value // Metrics collection Metrics *Metrics // Is AI logging enabled? // Current superloc Log struct { Enabled bool MaxSuperloc *int MaxPointsToSize *int MaxMemHeight *int Superloc defs.Superloc CtrLocVisits map[defs.Superloc]map[defs.Goro]map[defs.CtrLoc]*struct { // contains filtered or unexported fields } SuperlocationsFound map[defs.Superloc]struct{} // contains filtered or unexported fields } }
func (AnalysisCtxt) Blacklisted ¶
func (C AnalysisCtxt) Blacklisted(callIns ssa.CallInstruction, sfun *ssa.Function) bool
func (AnalysisCtxt) CheckMaxSuperloc ¶
func (C AnalysisCtxt) CheckMaxSuperloc(s defs.Superloc, spawnee defs.Goro)
func (AnalysisCtxt) CheckMemory ¶
func (C AnalysisCtxt) CheckMemory(m L.Memory)
func (AnalysisCtxt) CheckPointsTo ¶
func (C AnalysisCtxt) CheckPointsTo(v L.PointsTo)
func (*AnalysisCtxt) FragmentPredicateFromPrimitives ¶
func (C *AnalysisCtxt) FragmentPredicateFromPrimitives( primitives []ssa.Value, primitiveToUses map[ssa.Value]map[*ssa.Function]struct{}, )
Computes a fragment predicate that includes all functions on paths to concurrency operations that use the provided primitives, including their allocation.
func (AnalysisCtxt) IsPrimitiveFocused ¶
func (C AnalysisCtxt) IsPrimitiveFocused(prim ssa.Value) bool
func (AnalysisCtxt) LogCtrLocMemory ¶
func (AnalysisCtxt) LogSuperlocation ¶
func (C AnalysisCtxt) LogSuperlocation(sl defs.Superloc)
func (*AnalysisCtxt) LogWildcardSwap ¶
func (C *AnalysisCtxt) LogWildcardSwap(m L.Memory, l loc.Location)
func (AnalysisCtxt) TopInjectParams ¶
func (C AnalysisCtxt) TopInjectParams( callIns ssa.CallInstruction, g defs.Goro, state L.AnalysisState, blacklists map[*ssa.Function]struct{}) L.Memory
type BaseConfiguration ¶
func (*BaseConfiguration) AddSuccessor ¶
func (s *BaseConfiguration) AddSuccessor(succ Successor)
func (*BaseConfiguration) GetSuccessorMap ¶
func (s *BaseConfiguration) GetSuccessorMap() map[uint32]Successor
type Blocks ¶
func BlockAnalysis ¶
func BlockAnalysis(C AnalysisCtxt, G SuperlocGraph, result L.Analysis) (res Blocks)
func (Blocks) UpdateWith ¶
UpdateWith joins the results of `other` into `o`.
type Configuration ¶
type Configuration interface { AbstractionLevel() ABSTRACTION_LEVEL Init(ABSTRACTION_LEVEL) Configuration String() string PrettyPrint() IsSynchronizing(AnalysisCtxt, L.AnalysisState) bool AddSuccessor(Successor) GetSuccessorMap() map[uint32]Successor GetTransitions(AnalysisCtxt, L.AnalysisState) transfers Abstract(ABSTRACTION_LEVEL) Configuration Visualize() }
func NewConfiguration ¶
func NewConfiguration(abs ABSTRACTION_LEVEL) Configuration
type ConfigurationSuccessors ¶
func (ConfigurationSuccessors) PrettyPrint ¶
func (S ConfigurationSuccessors) PrettyPrint()
type FragmentPredicate ¶
type FragmentPredicate = func(ssa.CallInstruction, *ssa.Function) bool
type Metrics ¶
type Metrics struct { Outcome string // contains filtered or unexported fields }
func (*Metrics) AddCallees ¶
func (m *Metrics) AddCallees(callIns ssa.CallInstruction, calleeSet funset)
func (*Metrics) CallsiteCallees ¶
func (m *Metrics) CallsiteCallees() map[ssa.CallInstruction]funset
func (*Metrics) Chans ¶
func (m *Metrics) Chans() map[ssa.Instruction]struct{}
func (*Metrics) ConcurrencyOps ¶
func (m *Metrics) ConcurrencyOps() map[ssa.Instruction]struct{}
func (*Metrics) ExpandFunction ¶
func (*Metrics) Gos ¶
func (m *Metrics) Gos() map[ssa.Instruction]struct{}
func (*Metrics) HasConcurrency ¶
func (*Metrics) IsRelevant ¶
func (*Metrics) MaxCallees ¶
func (m *Metrics) MaxCallees() (ins ssa.CallInstruction, max int)
func (*Metrics) Performance ¶
func (*Metrics) TimerStart ¶
func (m *Metrics) TimerStart()
type Successor ¶
type Successor struct {
// contains filtered or unexported fields
}
Basic successor implementation for any configuration. Successors at different abstraction levels should embed it. Includes a description of the transition, and the succeeding configuration.
func (Successor) Configuration ¶
func (succ Successor) Configuration() *AbsConfiguration
func (Successor) DeriveConf ¶
func (succ Successor) DeriveConf(c *AbsConfiguration) Successor
func (Successor) PrettyPrint ¶
func (succ Successor) PrettyPrint()
func (Successor) Transition ¶
func (succ Successor) Transition() T.Transition
type SuperlocGraph ¶
type SuperlocGraph struct {
// contains filtered or unexported fields
}
func StaticAnalysis ¶
func StaticAnalysis(C AnalysisCtxt) (SuperlocGraph, L.Analysis)
Harness for performing fully static analysis. Accepts entry abstract configuration node as input and generates an analysis result.
func (SuperlocGraph) Entry ¶
func (G SuperlocGraph) Entry() *AbsConfiguration
func (SuperlocGraph) ForEach ¶
func (G SuperlocGraph) ForEach(do func(*AbsConfiguration))
func (SuperlocGraph) Get ¶
func (G SuperlocGraph) Get(s *AbsConfiguration) *AbsConfiguration
func (SuperlocGraph) PrettyPrint ¶
func (G SuperlocGraph) PrettyPrint()
func (SuperlocGraph) Size ¶
func (G SuperlocGraph) Size() int
func (SuperlocGraph) String ¶
func (G SuperlocGraph) String() (str string)
func (SuperlocGraph) Terminals ¶
func (G SuperlocGraph) Terminals() map[*AbsConfiguration]struct{}
Returns all terminal configurations
func (SuperlocGraph) ToGraph ¶
func (G SuperlocGraph) ToGraph() graph.Graph[*AbsConfiguration]