go-air / pal Goto Github PK

Tasks:

• creation
• #45
• map update, lookup
• slice indexing
• interfaces
• plain serialise
• channels

Initial prototyping has changed a number of design elements.

• #34
  - [x] analyzer framework stub
  - [ ] service
• #35
  - [x] constraints (load, store, transfer)
  - [x] plain serialize
  - [ ] solve
  - [ ] solve with opaque bindings
  - [ ] export
  - [ ] import
• #36
  - [ ] integrate types
  - [ ] dev.typeparams version
• #37
  - [ ] to go types
  - [x ] from go types
  - [x ] serialize
• #40
  - [x] creation
  - [ ] function call
  - [x] map update, lookup
  - [x] slice indexing
• #38
  - [x] loads
  - [x] stores
  - [x] map values to memory locations
  - [x] map values to objects
  - [ ] indexing arithmetic operations
  - [x] structs
  - [x] arrays
  - [ ] slices
  - [x] returns
  - [x] phi nodes
  - [x] function objects
  - [ ] function variadics
  - [ ] builtins
  - [x] range/next iterations.
• #39
  - [x] statement of purpose
  - [ ] design
  - [ ] cli
  - [ ] service
  - [ ] tutorial
  - [ ] reference

• constraints (load, store, transfer)
• plain serialize
• integrate types. memory model currently uses go/types and should use typeset instead.
• solve
• solve with opaque bindings
• export
• import

Function calls

• static dispatch of user code
• static dispatch builtins
• dispatch of *ssa.MakeClosure
• dynamic dispatch
• method calls by interface (invoke)

• stores
• map values to memory locations
• map values to objects
• indexing arithmetic operations
• structs
• arrays
• slices
• loads
• returns
• phi nodes
• function objects
• function variadics
• builtins
• range/next

• statement of purpose
• design
  • cli
  • service
• tutorial
• reference

• analyzer framework stub
• service

golang/go#47725 highlights some problems with the serialisation and filtering mechanism of Facts in go's analysis library.

This issue is here to track how pal interacts with it.

At this time, pal has only been tested as a single/multi checker, and we have tried to work around the whole fact mechanism as it does not seem to fit pal's needs.

Add constraint indexing to all opaque locs so that all constraints involving them can be re-applied under different substitions.

• dev.typeparams version.
• integrate types.
• constants (integrate go/constant).
• plain serialise.

Implement a naive solver for which we have a good level of confidence in correctness. This will be a baseline.

Make a pass over go/ssa form, extract all heap allocations (including things such as varargs), model and index them with mems.

(This was perhaps underestimated in effort, typical of a first prototype...)

I think it will be worthwhile to reduce the scope and make things more explicit.

• globals
• locals
• stores
• field address
• #14
• #15

Encode constraints into the memory model from the ssa.

We need to decide on how to accept IP.

• to go types
• from go types
• serialize
• testing.