@@ -10,7 +10,7 @@ specific to control flow and/or call flow context. However, pal leaves this
1010opaque to the user, at least at the level of the memory model.
1111
1212Sets of locs may or may not support non-constant values for their size. For non-constant
13- values which occur in the program under analysis, a special Value type is provided and
13+ index which occur in the program under analysis, a special Value type is provided and
1414detailed below.
1515
1616Sets of locs must provide an efficient means to determine if two locs 'm', 'n' may overlap
@@ -29,7 +29,7 @@ and/or locations in the program of heap allocations such as `malloc`.
2929
3030In Go's x/tools/go/pointer, a loc correponds to a node, so for example a
3131map would would be represented by a node representing a (key, value) pair;
32- all the values in the map are abstracted to a single pair.
32+ all the index in the map are abstracted to a single pair.
3333
3434For flow sensitivity, an SSA form in combination with such a representation
3535can be used. For more flow sensitivity an SSI form can be used. These
@@ -50,18 +50,18 @@ type Constraints interface {
5050}
5151```
5252
53- ## Values
53+ ## index
5454
5555Traditional pointer analyses such as Anderson, SteensGaard are independent of
5656numerical analysis. Often such analysis are useful because they can bootstrap a
5757numerical analysis and they are usually much faster (albeit less precise) than
5858methods which combine numerical and points-to analysis.
5959
60- pal provides opaque support for numerical constraints in a _ Values _ type, defined
60+ pal provides opaque support for numerical constraints in a _ index _ type, defined
6161below.
6262
6363``` go
64- type Values interface {
64+ type index interface {
6565 ToInt (v Value ) (int , bool )
6666 FromInt (int ) V
6767 Plus (a, b Value ) Value
@@ -72,19 +72,19 @@ type Values interface {
7272
7373
7474The idea is that the pointer operations only use addition and tests for
75- Values in order to implement the Mems interface; however, Values in programs
75+ index in order to implement the Mems interface; however, index in programs
7676may be arbitrary expressions in the target language, which, over the
7777set of all possible executions of the program, may contain any sort of
7878concrete value.
7979
80- A client of pal must decide how to model these concrete values , however any such
81- model will provide the Values interface above.
80+ A client of pal must decide how to model these concrete index , however any such
81+ model will provide the index interface above.
8282
8383pal will provide some basic models
8484
85- ### Const Values
85+ ### Const index
8686
87- Constant values , corresponding to types\' offsets. In this model, every load or store
87+ Constant index , corresponding to types\' offsets. In this model, every load or store
8888to a Mem with non-constant offset are collapsed onto a single Mem with zero offset.
8989This is an abstraction which is simple, efficient, and imprecise for containers
9090containing lots of pointers.
@@ -96,54 +96,68 @@ generated.
9696
9797TODO(wsc0)
9898
99- ## Solving
100-
101- Suppose we have a program or a fragment of a program for which we have created
102- Mems, Constraints, and Values. We would like to compute the points to set of
103- Mems
99+ ## Modularity
104100
105- In pal, all these scenarios share a common _ Solver_ interface specified below.
101+ Pal follows Go's packages, which form an acyclic dependency graph. Pal
102+ results are stored on a per-package basis.
106103
107104
108- ``` go
105+ ### Coding
109106
110- // Construct a solver from Mems (and so with the associated constraints)
111- // and a modelling of the values. Results are precomputed.
112- func SolverForAll (ms Mems , vs Values ) Solver
113- // Results are on demand.
114- func LazySolver(ms Mems, vs Values) Solver
115- // Results are pre-ordered according to 'perm'
116- func OrderedSolver(ms Mems, []int perm, vs Values) Solver
107+ This consists of encoding the package into the pal memory model.
108+ Notably, for modularity, we need to keep track of exportable
109+ symbols, opaqueness, param and return index of functions.
117110
118- // Results are selected from q and PointsTo means transitively to
119- // things related to q (forward and backward )
120- func SelectFwdSolver(ms Mems, q []Mem, vs Values) Solver {...}
121- func SelectBwdSolver (ms Mems , q []Mem , vs Values ) Solver {...}
122- func SelectSolve (ms Mems , q []Mem , vs Values ) Solver {...}
111+ ### Solving
123112
124- // project the transitive closue of the points to onto 'on'
125- func ProjectedSolver ( ms Mems , on [] Mem , vs Values ) Solver
113+ This consists of finding the points- to relation for the package
114+ in terms of how it was coded.
126115
127- type Solver interface {
116+ ### Export
128117
129- // Overlaps determines complex aliasing.
130- Overlaps (m Mem, mext Value, n Mem, next Value) AbsTruth
118+ This consists of projecting the memory model onto i/o relations
119+ between exported opaque memory locations (including parameters
120+ and returns of exported functions).
131121
132- // m == n ?
133- Equal (m, n Mem) AbsTruth
122+ ### Import
134123
135124
136- // PointsTo place the points to set of m into dst, starting
137- // at offset from with a max of 'ext',
138- //
139- // return the resulting dst.
140- PointsTo (dst []Mem, m Mem, ext Value) []Mem
125+ ### Example
141126
142- // ReplaceOpaque
143- // for every Mem in the underlying Mems whose points-to set
144- // includes the points to set of 't', remove the points-to
145- // set of 't' and add the PointsTo set of every rep in 'reps'
146- ReplaceOpaque (t Mem, reps ...Mem )
127+ Below is an example diamond
128+ shaped package dependency graph which we will use to describe how
129+ modular solving works.
147130
148- }
149131```
132+ S -> A
133+ S -> B
134+ A -> D
135+ B -> D
136+ ```
137+ Below is a list of actions for solving the points-to
138+ incrementally
139+
140+
141+ 1 . D: Code
142+ 1 . D: Solve
143+ 1 . D: Export
144+ 1 . A: Import D
145+ 1 . A: Code
146+ 1 . A: Solve
147+ 1 . A: Export
148+ 1 . B: Import D
149+ 1 . B: Code
150+ 1 . B: Solve
151+ 1 . B: Export
152+ 1 . S: Import A
153+ 1 . S: Import B
154+ 1 . S: Code
155+ 1 . S: Solve
156+
157+
158+
159+
160+ ## Solving
161+
162+
163+
0 commit comments