constraint

Documentation

Index

• Variables
• func Is_Value_the_same(a, b ssa.Value) bool
• func Is_two_bb_definitely_both_happen(a, b ssa.BasicBlock) bool
• func SMT_of_two_bb_precondition_the_same_locally(bb1, bb2 *ssa.BasicBlock) (*SMT_set, *SMT_set)
• func Type_of_value(v ssa.Value) string
• type Assert
• type Dec_const
• type Dec_fn
• type Dec_sort
• type Define_sort
• type SMT_set
  • func Conds2SMT_set(conds []path.Cond) (result *SMT_set)
  • func Union_two_SMTs(s1, s2 *SMT_set) (result *SMT_set)
  • func (s *SMT_set) Print_body()
  • func (s *SMT_set) Print_tail()

Variables

var (
	SMT_Bool      = "Bool"
	SMT_EQL       = "="
	SMT_not       = "not"
	Default_sorts = []string{"byte", "int", "int64", "bool", "string"}
)

Functions

func Is_Value_the_same

func Is_Value_the_same(a, b ssa.Value) bool

This is my own solver that can compare two ssa.Value. It can only consider part of types of ssa.Value and only works when two values are almost the same

func Is_two_bb_definitely_both_happen

func Is_two_bb_definitely_both_happen(a, b ssa.BasicBlock) bool

TODO: Now it can only deal with circumstances like: if(cond1) then bb1 endif; ... no return ... ; if(cond1) then bb2 endif;

func SMT_of_two_bb_precondition_the_same_locally

func SMT_of_two_bb_precondition_the_same_locally(bb1, bb2 *ssa.BasicBlock) (*SMT_set, *SMT_set)

func Type_of_value

func Type_of_value(v ssa.Value) string

Types

type Assert

type Assert string

type Dec_const

type Dec_const struct {
	Name  string
	Type  string
	Value ssa.Value
}

type Dec_fn

type Dec_fn struct {
	Name    string
	Inputs  []string
	Outputs []string
}

type Dec_sort

type Dec_sort struct {
	Name string
}

type Define_sort

type Define_sort struct {
	Name             string
	Input            string
	Output           string
	Has_input_output bool
}

type SMT_set

type SMT_set struct {
	Dec_sorts    []Dec_sort
	Dec_fns      []Dec_fn
	Define_sorts []Define_sort
	Dec_consts   []Dec_const
	Asserts      []Assert
	Final_const  Dec_const
	Final_Assert Assert
	Todo         []ssa.Value
	Status       string
	Index        int
}

func Conds2SMT_set

func Conds2SMT_set(conds []path.Cond) (result *SMT_set)

func Union_two_SMTs

func Union_two_SMTs(s1, s2 *SMT_set) (result *SMT_set)

func (*SMT_set) Print_body

func (s *SMT_set) Print_body()

Print_body prints everything in order except the last assert and "check-sat"

func (*SMT_set) Print_tail

func (s *SMT_set) Print_tail()