Documentation ¶
Overview ¶
Package memory defines the memory model of pal and associated operations.
The memory model is basically a directed graph, where the nodes represent disjoint memory regions (such as the locations of local variables, or the code location of an allocation), and the edges represents a "may points to" relation. In other words for nodes a,b where (a,b) is an edge, the memory model indicates that in some execution of the analysed program, a may point to b.
Separate memory models are intended to be associated with every package under analysis.
The above description is a simplification of what is implemented here. First, nodes represent structured data (arrays and structs). Second, the edges are coded as a set of constraints rather than explicitly. Third, the node sizes are parameterised on a index type which may be used to model sizes and indices.
Finally, some nodes are marked "Opaque" indicating that they represent unknown pointers. Correspondingly, there is a (work in progress) mechanism to compose models accross packages which allows eliminating local variables and substituting opaque nodes with results in a calling package.
Locs ¶
Memory locations are the fundamental unit of a memory model, defined in the type Loc as a uint32. Each location has a root, and root locations represent canonical memory regions. A region is disjoint from another region if the associated roots are not identical.
Internally, Locs have this structure:
type loc struct { class ... attrs ... root Loc; parent Loc; lsz int; typ typeset.Type }
The values of this internal structure are only accessible from the Model type. Memory location classes indicate whether the memory is global, local (stack), or heap allocated. Memory location attributes indicate whether a location corresponds to a parameter, a return, and whether it is opaque.
Structured Data ¶
Data structuring models structs and arrays (but not slices or maps) and how such data types map to contiguous memory regions. A logical size is associated with each location, and is defined by the type associated with the data. For struct 's' with fields '[f1, f2, ...]', the models contain one location for 's': 'loc(s)', and one location for each field 'fi': loc(fi). The virtual size of 'loc(s)' is equal to 1 + the sum of the virtual sizes for the fields. Array work likewise, keyed by constant index. Non structured types have size '1 + Sum(lsz children) == 1'
Each location 'm' in structured data has a root node acting as an identifier for its region and a parent node, indicating to what structure it belongs. The parent pointers are self-loops for roots.
Constraints ¶
Each model has a set of associated constraints. Constraints have a collecting semantics (they act like generators or production rules in a grammar).
PointsTo constraints 'p = &v' indicate that v is in the points to set of p.
Load constraints 'd = *p' indicate that for any v in the points to set of p, the points-to set of v is contained in in the points to set of d, recursively descending structured data at *p in tandem with d.
Store constraints '*p = v' indicate that for any d in the points to set of p and any w in the points to set of v, w is in the points to set of d, recursively descending structured data at v, in tandem with d.
Transfer constraints 'dst = src + i' indicate the points to set of src at index i is contained in the points to set of dst. i may either be a constant or an expression from the program under analysis. i must be the constant 0 for any pointer to a basic type. i must be a constant if src is a pointer to a struct. i may be an int64 expression if src is a pointer to an array or slice.
Index ¶
- Constants
- type Attrs
- type Class
- type Constraint
- type ConstraintKind
- type GenParams
- type Loc
- type Model
- func (mod *Model) AddAddressOf(a, b Loc)
- func (mod *Model) AddAttrs(m Loc, a Attrs)
- func (mod *Model) AddLoad(dst, src Loc)
- func (mod *Model) AddStore(dst, src Loc)
- func (mod *Model) AddTransfer(dst, src Loc)
- func (mod *Model) AddTransferIndex(dst, src Loc, i indexing.I)
- func (mod *Model) ArrayIndex(m Loc, i int) Loc
- func (mod *Model) At(i int) Loc
- func (mod *Model) Attrs(m Loc) Attrs
- func (mod *Model) Cap(c int)
- func (mod *Model) Equals(a, b Loc) xtruth.T
- func (mod *Model) Export(perm []Loc) []Loc
- func (mod *Model) Field(m Loc, i int) Loc
- func (mod *Model) Gen(gp *GenParams) Loc
- func (mod *Model) Import(other *Model)
- func (mod *Model) IsRoot(m Loc) bool
- func (mod *Model) Len() int
- func (mod *Model) Lsize(m Loc) int
- func (mod *Model) Obj(ptr Loc) Loc
- func (mod *Model) Overlaps(a, b Loc) xtruth.T
- func (mod *Model) Parent(m Loc) Loc
- func (mod *Model) PlainCoderAt(i int) plain.Coder
- func (mod *Model) PlainDecode(r io.Reader) error
- func (mod *Model) PlainDecodeConstraints(r io.Reader) error
- func (mod *Model) PlainEncode(w io.Writer) error
- func (mod *Model) PlainEncodeConstraints(w io.Writer) error
- func (mod *Model) PointsToFor(dst []Loc, p Loc) []Loc
- func (mod *Model) Pos(m Loc) token.Pos
- func (mod *Model) Root(m Loc) Loc
- func (mod *Model) SetAttrs(m Loc, a Attrs)
- func (mod *Model) SetObj(ptr, dst Loc)
- func (mod *Model) Solve()
- func (mod *Model) Type(m Loc) typeset.Type
- func (mod *Model) WithPointer(gp *GenParams) (obj, ptr Loc)
- func (mod *Model) Zero() Loc
Constants ¶
const NoLoc = Loc(0)
Variables ¶
This section is empty.
Functions ¶
This section is empty.
Types ¶
type Constraint ¶
type Constraint struct { Kind ConstraintKind Dest Loc Src Loc Index indexing.I }
func AddressOf ¶
func AddressOf(dst, src Loc) Constraint
func Load ¶
func Load(dst, src Loc) Constraint
func Store ¶
func Store(dst, src Loc) Constraint
func TransferIndex ¶
func TransferIndex(dst, src Loc, i indexing.I) Constraint
func (*Constraint) PlainDecode ¶
func (c *Constraint) PlainDecode(r io.Reader) error
func (*Constraint) PlainEncode ¶
func (c *Constraint) PlainEncode(w io.Writer) error
type ConstraintKind ¶
type ConstraintKind int
const ( KAddressOf ConstraintKind = iota KLoad KStore KTransfer )
func (*ConstraintKind) PlainDecode ¶
func (ck *ConstraintKind) PlainDecode(r io.Reader) error
func (ConstraintKind) PlainEncode ¶
func (ck ConstraintKind) PlainEncode(w io.Writer) error
type GenParams ¶ added in v0.0.3
type GenParams struct {
// contains filtered or unexported fields
}
GenParams encapsulates the information needed for a memory model to generate memory locations.
func NewGenParams ¶ added in v0.0.3
type Loc ¶
type Loc uint32
Loc represents a memory location.
This memory location is intented for pal points to analysis. it has nothing to do with the numeric value of a pointer in a program.
type Model ¶
type Model struct {
// contains filtered or unexported fields
}
Type Model represents a memory model for a package.
func NewModel ¶
NewModel generates a new memory model for a package.
index parameterises the resulting model on numeric (int) indexing.
func (*Model) ArrayIndex ¶
ArrayIndex returns the memory model location of `m` at index `i`.
func (*Model) Export ¶
Export exports the model 'mod', removing unnecessary local mem.Locs and compacting the result by permuting the remaining locations. Export returns the permutation if 'perm' is non-nil.
Generally, after Export is called, 'mod' contains no local variables. One can retrieve points-to information for local variables using PoinstToFor, before calling Export.
func (*Model) Lsize ¶ added in v0.0.3
Lsize returns the virtual size of memory associated with m.
The virtual size is the size according to the model, which is 1 + the sum of the the vsizes of all locations n such that mod.Parent(n) == m.
func (*Model) PlainCoderAt ¶
PlainCoderAt returns a plain.Coder for the information associated with memory at index i.
func (*Model) PointsToFor ¶
PointsTo places the points-to set of p in dst and returns it.