solver

Documentation

Index

• type Branch
• type BranchDeref
  • func (b *BranchDeref) Instr() ssa.Instruction
  • func (b *BranchDeref) Other() *ssa.BasicBlock
  • func (b *BranchDeref) To() *ssa.BasicBlock
• type BranchIf
  • func (b *BranchIf) Instr() ssa.Instruction
  • func (b *BranchIf) Other() *ssa.BasicBlock
  • func (b *BranchIf) To() *ssa.BasicBlock
• type Definite
  • func (s Definite) Concretize(f func(types.Type) interface{}) interface{}
  • func (s Definite) Type() types.Type
• type Indefinite
  • func NewIndefinite(ty types.Type) Indefinite
  • func (s Indefinite) Concretize(f func(types.Type) interface{}) interface{}
  • func (s Indefinite) Type() types.Type
• type Solution
• type UnsatError
  • func (ue UnsatError) Error() string
• type Z3Solver
  • func CreateZ3Solver(symbols []ssa.Value, instrs []ssa.Instruction, isComplete bool) (*Z3Solver, error)
  • func (s *Z3Solver) Branch(i int) Branch
  • func (s *Z3Solver) Branches() []Branch
  • func (s *Z3Solver) Close()
  • func (s *Z3Solver) NumBranches() int
  • func (s *Z3Solver) Solve(negate int) ([]Solution, error)

Types

type Branch

type Branch interface {
	// Instr returns ssa.Instruction value for the branch.
	Instr() ssa.Instruction

	// To returns ssa.BasicBlock that the branch took.
	To() *ssa.BasicBlock

	// Other returns ssa.BasicBlock that the branch did not take.
	Other() *ssa.BasicBlock
}

Branch represents a branch appeared in a running trace. This includes instructions that may cause a panic (e.g., pointer dereference) as well as ordinary branching by *ssa.If.

type BranchDeref

type BranchDeref struct {
	// contains filtered or unexported fields
}

BranchDeref represents a branching (success or panic) caused by dereference (*ssa.UnOp or *ssa.FieldAddr).

func (*BranchDeref) Instr

func (b *BranchDeref) Instr() ssa.Instruction

Instr returns ssa.Instruction value for the branch.

func (*BranchDeref) Other

func (b *BranchDeref) Other() *ssa.BasicBlock

Other returns ssa.BasicBlock that the branch did not take.

func (*BranchDeref) To

func (b *BranchDeref) To() *ssa.BasicBlock

To returns ssa.BasicBlock that the branch took.

type BranchIf

type BranchIf struct {
	// contains filtered or unexported fields
}

BranchIf contains a branching instruction (*ssa.If) and the direction taken in the concolic execution.

func (*BranchIf) Instr

func (b *BranchIf) Instr() ssa.Instruction

Instr returns ssa.Instruction value for the branch.

func (*BranchIf) Other

func (b *BranchIf) Other() *ssa.BasicBlock

Other returns ssa.BasicBlock that the branch did not take.

func (*BranchIf) To

func (b *BranchIf) To() *ssa.BasicBlock

To returns ssa.BasicBlock that the branch took.

type Definite

type Definite struct {
	// contains filtered or unexported fields
}

Definite represents a solution. If ty is *types.Pointer, then the value is an instance of Solution which represents the referenced value.

func (Definite) Concretize

func (s Definite) Concretize(f func(types.Type) interface{}) interface{}

Concretize returns the value.

func (Definite) Type

func (s Definite) Type() types.Type

Type returns type.

type Indefinite

type Indefinite struct {
	// contains filtered or unexported fields
}

Indefinite represents an indefinite solution.

func NewIndefinite

func NewIndefinite(ty types.Type) Indefinite

NewIndefinite returns a new indefinite solution.

func (Indefinite) Concretize

func (s Indefinite) Concretize(f func(types.Type) interface{}) interface{}

Concretize returns the value.

func (Indefinite) Type

func (s Indefinite) Type() types.Type

Type returns type.

type Solution

type Solution interface {
	Type() types.Type
	Concretize(func(types.Type) interface{}) interface{}
}

Solution represents a solution for a symbol.

type UnsatError

type UnsatError struct{}

UnsatError is an error describing that Z3 constraints were unsatisfied.

func (UnsatError) Error

func (ue UnsatError) Error() string

type Z3Solver

type Z3Solver struct {
	// contains filtered or unexported fields
}

Z3Solver is a type that holds the Z3 context, assertions, and symbols.

func CreateZ3Solver

func CreateZ3Solver(symbols []ssa.Value, instrs []ssa.Instruction, isComplete bool) (*Z3Solver, error)

CreateZ3Solver returns a new Z3Solver.

func (*Z3Solver) Branch

func (s *Z3Solver) Branch(i int) Branch

Branch returns the i-th branch instruction.

func (*Z3Solver) Branches

func (s *Z3Solver) Branches() []Branch

Branches returns the slice of branches.

func (*Z3Solver) Close

func (s *Z3Solver) Close()

Close deletes the Z3 context.

func (*Z3Solver) NumBranches

func (s *Z3Solver) NumBranches() int

NumBranches returns the number of branch instructions.

func (*Z3Solver) Solve

func (s *Z3Solver) Solve(negate int) ([]Solution, error)

Solve solves the assertions and returns concrete values for symbols. The condition to solve is p_0 /\ p_1 /\ ... /\ p_(k-1) /\ not(a_k) where p_i is a predicate of the i-th branching instruction and k = negate.