Abstract interpretation

[riadas]

No description provided.

[codecov-commenter]

Codecov Report

Patch coverage: 66.88% and project coverage change: +5.60 🎉

Comparison is base (d6e2684) 28.20% compared to head (6976552) 33.80%.

❗ Your organization is not using the GitHub App Integration. As a result you may experience degraded service beginning May 15th. Please install the Github App Integration for your organization. Read more.

Additional details and impacted files

@@            Coverage Diff             @@
##           master      #26      +/-   ##
==========================================
+ Coverage   28.20%   33.80%   +5.60%     
==========================================
  Files           6        7       +1     
  Lines        1195     1337     +142     
==========================================
+ Hits          337      452     +115     
- Misses        858      885      +27     

Impacted Files	Coverage Δ
src/Autumn.jl	100.00% <ø> (ø)
src/interpreter/autumnstdlib.jl	4.45% <ø> (+0.31%)	⬆️
src/interpreter/abstractinterpret.jl	46.93% <46.93%> (ø)
src/interpreter/interpretutils.jl	49.47% <50.00%> (-0.13%)	⬇️
src/interpreter/interpret.jl	75.24% <77.55%> (+0.24%)	⬆️

... and 1 file with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Do you have feedback about the report comment? Let us know in this issue.

[riadas]

Completed milestone 1: If the second argument to prev is a literal, e.g. (prev food 3), then the history tracking depth for that variable is set to that literal. If the second argument is any other expression, history tracking depth is set to Inf for now (to be updated upon implementation of abstract interpretation). If no second argument is used in prev calls on a variable, the history tracking depth for that variable defaults to 1.

[riadas]

For context, milestone 1 means that we can interpret the below Fibonacci program, with two past history values tracked for the variable x rather than the full history.

(program
  (= x (initnext 1 (+ (prev x 2) (prev x))))
)

[riadas]

Completed version of milestone 2, which means the below programs are now successively interpreted:

(program
   (= x (initnext 1 (+ (prev x (+ 1 1)) (prev x)))
)

(program
   (= offset (initnext 2 (prev offset)))
   (= x (initnext 1 (+ (prev x offset) (prev x)))
)

(program
   (= offset (initnext 1 (prev offset)))
   (= x (initnext 1 (+ (prev x (+ offset offset)) (prev x)))
)

[riadas]

The below program

(program
  (= y (initnext 2 (+ (prev y (+ 0 1)) 0)))
  (= x (initnext 2 (prev x y)))
  (= z (initnext 1 (+ (prev z) (prev z x))))
)

is transformed into

(program
  (on true (= z (+ (prev z) (prev z 2))))
)

by the abstract interpretation procedure, which also initializes y = 2, x = 2, z = 1 into the environment. The lines corresponding to x and y updates are removed since they were identified as constants. The history depths are

Dict{Symbol,Union{Float64, Int64}} with 3 entries:
  :y => 1
  :z => 2
  :x => 1

and the result of 10 time steps of interpretation are

julia> interpret_over_time(aex, 10, []).state.histories
Dict{Symbol,Dict{Int64,Any}} with 4 entries:
  :GRID_SIZE => Dict{Int64,Any}(0=>16)
  :y         => Dict{Int64,Any}(10=>2)
  :z         => Dict{Int64,Any}(9=>89,10=>144)
  :x         => Dict{Int64,Any}(10=>2)