agda-spa/Analysis/Forward.agda

369 lines
20 KiB
Agda
Raw Normal View History

open import Language hiding (_[_])
open import Lattice
module Analysis.Forward
{L : Set} {h}
{_≈ˡ_ : L L Set} {_⊔ˡ_ : L L L} {_⊓ˡ_ : L L L}
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_)
(≈ˡ-dec : IsDecidable _≈ˡ_) where
open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Nat using (suc)
open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Data.Sum using (inj₁; inj₂)
open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using ()
open import Function using (_∘_; flip)
import Chain
open import Utils using (Pairwise; _⇒_; __)
import Lattice.FiniteValueMap
open IsFiniteHeightLattice isFiniteHeightLatticeˡ
using ()
renaming
( isLattice to isLatticeˡ
; fixedHeight to fixedHeightˡ
; _≼_ to _≼ˡ_
; ≈-sym to ≈ˡ-sym
)
module WithProg (prog : Program) where
open Program prog
-- The variable -> abstract value (e.g. sign) map is a finite value-map
-- with keys strings. Use a bundle to avoid explicitly specifying operators.
module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
open VariableValuesFiniteMap
using ()
renaming
( FiniteMap to VariableValues
; isLattice to isLatticeᵛ
; _≈_ to _≈ᵛ_
; _⊔_ to _⊔ᵛ_
; _≼_ to _≼ᵛ_
; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec
; _∈_ to _∈ᵛ_
; _∈k_ to _∈kᵛ_
; _updating_via_ to _updatingᵛ_via_
; locate to locateᵛ
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ
; ∈k-dec to ∈k-decᵛ
; all-equal-keys to all-equal-keysᵛ
)
public
open IsLattice isLatticeᵛ
using ()
renaming
( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ
; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
; ⊔-idemp to ⊔ᵛ-idemp
)
open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ
using ()
renaming
( Provenance-union to Provenance-unionᵐ
)
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
using ()
renaming
( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
)
≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
-- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
open StateVariablesFiniteMap
using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
renaming
( FiniteMap to StateVariables
; isLattice to isLatticeᵐ
; _≈_ to _≈ᵐ_
; _∈_ to _∈ᵐ_
; _∈k_ to _∈kᵐ_
; locate to locateᵐ
; _≼_ to _≼ᵐ_
; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
)
public
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
using ()
renaming
( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
)
open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
using ()
renaming
( ≈-sym to ≈ᵐ-sym
)
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
-- We now have our (state -> (variables -> value)) map.
-- Define a couple of helpers to retrieve values from it. Specifically,
-- since the State type is as specific as possible, it's always possible to
-- retrieve the variable values at each state.
states-in-Map : (s : State) (sv : StateVariables) s ∈kᵐ sv
states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s
variablesAt : State StateVariables VariableValues
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-∈ : (s : State) (sv : StateVariables) (s , variablesAt s sv) ∈ᵐ sv
variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-≈ : s sv₁ sv₂ sv₁ ≈ᵐ sv₂ variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
(states-in-Map s sv₁) (states-in-Map s sv₂)
-- build up the 'join' function, which follows from Exercise 4.26's
--
-- L₁ → (A → L₂)
--
-- Construction, with L₁ = (A → L₂), and f = id
joinForKey : State StateVariables VariableValues
joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
-- The per-key join is made up of map key accesses (which are monotonic)
-- and folds using the join operation (also monotonic)
joinForKey-Mono : (k : State) Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
(m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
(⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
-- The name f' comes from the formulation of Exercise 4.26.
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x x) (λ a₁≼a₂ a₁≼a₂) joinForKey joinForKey-Mono states
renaming
( f' to joinAll
; f'-Monotonic to joinAll-Mono
; f'-k∈ks-≡ to joinAll-k∈ks-≡
)
variablesAt-joinAll : (s : State) (sv : StateVariables)
variablesAt s (joinAll sv) joinForKey s sv
variablesAt-joinAll s sv
with (vs , s,vs∈usv) locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll sv)) =
joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
-- With 'join' in hand, we need to perform abstract evaluation.
module WithEvaluator (eval : Expr VariableValues L)
(eval-Mono : (e : Expr) Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where
-- For a particular evaluation function, we need to perform an evaluation
-- for an assignment, and update the corresponding key. Use Exercise 4.26's
-- generalized update to set the single key's value.
private module _ (k : String) (e : Expr) where
open VariableValuesFiniteMap.GeneralizedUpdate vars isLatticeᵛ (λ x x) (λ a₁≼a₂ a₁≼a₂) (λ _ eval e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ eval-Mono e {vs₁} {vs₂} vs₁≼vs₂) (k [])
renaming
( f' to updateVariablesFromExpression
; f'-Monotonic to updateVariablesFromExpression-Mono
; f'-k∈ks-≡ to updateVariablesFromExpression-k∈ks-≡
; f'-k∉ks-backward to updateVariablesFromExpression-k∉ks-backward
)
public
-- The per-state update function makes use of the single-key setter,
-- updateVariablesFromExpression, for the case where the statement
-- is an assignment.
--
-- This per-state function adjusts the variables in that state,
-- also monotonically; we derive the for-each-state update from
-- the Exercise 4.26 again.
updateVariablesFromStmt : BasicStmt VariableValues VariableValues
updateVariablesFromStmt (k e) vs = updateVariablesFromExpression k e vs
updateVariablesFromStmt noop vs = vs
updateVariablesFromStmt-Monoʳ : (bs : BasicStmt) Monotonic _≼ᵛ_ _≼ᵛ_ (updateVariablesFromStmt bs)
updateVariablesFromStmt-Monoʳ (k e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂
updateVariablesFromStmt-Monoʳ noop vs₁≼vs₂ = vs₁≼vs₂
updateVariablesForState : State StateVariables VariableValues
updateVariablesForState s sv =
foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s)
updateVariablesForState-Monoʳ : (s : State) Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s)
updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ =
let
bss = code s
(vs₁ , s,vs₁∈sv₁) = locateᵐ {s} {sv₁} (states-in-Map s sv₁)
(vs₂ , s,vs₂∈sv₂) = locateᵐ {s} {sv₂} (states-in-Map s sv₂)
vs₁≼vs₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ sv₁ sv₂ sv₁≼sv₂ s,vs₁∈sv₁ s,vs₂∈sv₂
in
foldl-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss
(flip updateVariablesFromStmt) updateVariablesFromStmt-Monoʳ
vs₁≼vs₂
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x x) (λ a₁≼a₂ a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
renaming
( f' to updateAll
; f'-Monotonic to updateAll-Mono
; f'-k∈ks-≡ to updateAll-k∈ks-≡
)
-- Finally, the whole analysis consists of getting the 'join'
-- of all incoming states, then applying the per-state evaluation
-- function. This is just a composition, and is trivially monotonic.
analyze : StateVariables StateVariables
analyze = updateAll joinAll
analyze-Mono : Monotonic _≼ᵐ_ _≼ᵐ_ analyze
analyze-Mono {sv₁} {sv₂} sv₁≼sv₂ =
updateAll-Mono {joinAll sv₁} {joinAll sv₂}
(joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
-- The fixed point of the 'analyze' function is our final goal.
open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ analyze-Mono {m₁} {m₂} m₁≼m₂)
using ()
renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
public
variablesAt-updateAll : (s : State) (sv : StateVariables)
variablesAt s (updateAll sv) updateVariablesForState s sv
variablesAt-updateAll s sv
with (vs , s,vs∈usv) locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll sv)) =
updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
open LatticeInterpretation latticeInterpretationˡ
using ()
renaming
( ⟦_⟧ to ⟦_⟧ˡ
; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
; ⟦⟧-⊔- to ⟦⟧ˡ-⊔ˡ-
)
⟦_⟧ᵛ : VariableValues Env Set
⟦_⟧ᵛ vs ρ = {k l} (k , l) ∈ᵛ vs {v} (k , v) Language.∈ ρ l ⟧ˡ v
⟦⊥ᵛ⟧ᵛ∅ : ⊥ᵛ ⟧ᵛ []
⟦⊥ᵛ⟧ᵛ∅ _ ()
⟦⟧ᵛ-respects-≈ᵛ : {vs₁ vs₂ : VariableValues} vs₁ ≈ᵛ vs₂ vs₁ ⟧ᵛ vs₂ ⟧ᵛ
⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
(m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ =
let
(l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂
⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ
in
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
⟦⟧ᵛ-⊔ᵛ- : {vs₁ vs₂ : VariableValues} ( vs₁ ⟧ᵛ vs₂ ⟧ᵛ) vs₁ ⊔ᵛ vs₂ ⟧ᵛ
⟦⟧ᵛ-⊔ᵛ- {vs₁} {vs₂} ρ ⟦vs₁⟧ρ⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
with ⟦vs₁⟧ρ⟦vs₂⟧ρ
... | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ- {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
... | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ- {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
⟦⟧ᵛ-foldr : {vs : VariableValues} {vss : List VariableValues} {ρ : Env}
vs ⟧ᵛ ρ vs ∈ˡ vss foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
⟦⟧ᵛ-foldr {vs} {vs vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
⟦⟧ᵛ-⊔ᵛ- {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
⟦⟧ᵛ-foldr {vs} {vs' vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
⟦⟧ᵛ-⊔ᵛ- {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
(inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
InterpretationValid : Set
InterpretationValid = {vs ρ e v} ρ , e ⇒ᵉ v vs ⟧ᵛ ρ eval e vs ⟧ˡ v
module WithValidity (interpretationValidˡ : InterpretationValid) where
updateVariablesFromStmt-matches : {bs vs ρ₁ ρ₂} ρ₁ , bs ⇒ᵇ ρ₂ vs ⟧ᵛ ρ₁ updateVariablesFromStmt bs vs ⟧ᵛ ρ₂
updateVariablesFromStmt-matches {_} {vs} {ρ₁} {ρ₁} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-matches {_} {vs} {ρ₁} {_} (⇒ᵇ-← ρ₁ k e v ρ,e⇒v) ⟦vs⟧ρ {k'} {l} k',l∈vs' {v'} k',v'∈ρ₂
with k ≟ˢ k' | k',v'∈ρ₂
... | yes refl | here _ v _
rewrite updateVariablesFromExpression-k∈ks-≡ k e {l = vs} (Any.here refl) k',l∈vs' =
interpretationValidˡ ρ,e⇒v ⟦vs⟧ρ
... | yes k≡k' | there _ _ _ _ _ k'≢k _ = ⊥-elim (k'≢k (sym k≡k'))
... | no k≢k' | here _ _ _ = ⊥-elim (k≢k' refl)
... | no k≢k' | there _ _ _ _ _ _ k',v'∈ρ₁ =
let
k'∉[k] = (λ { (Any.here refl) k≢k' refl })
k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
in
⟦vs⟧ρ k',l∈vs k',v'∈ρ₁
updateVariablesFromStmt-fold-matches : {bss vs ρ₁ ρ₂} ρ₁ , bss ⇒ᵇˢ ρ₂ vs ⟧ᵛ ρ₁ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-fold-matches {bs bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ρ,bss'⇒ρ₂) ⟦vs⟧ρ =
updateVariablesFromStmt-fold-matches
{bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
(updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ)
updateVariablesForState-matches : {s sv ρ₁ ρ₂} ρ₁ , (code s) ⇒ᵇˢ ρ₂ variablesAt s sv ⟧ᵛ ρ₁ updateVariablesForState s sv ⟧ᵛ ρ₂
updateVariablesForState-matches =
updateVariablesFromStmt-fold-matches
updateAll-matches : {s sv ρ₁ ρ₂} ρ₁ , (code s) ⇒ᵇˢ ρ₂ variablesAt s sv ⟧ᵛ ρ₁ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
updateAll-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ
rewrite variablesAt-updateAll s sv =
updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ
stepTrace : {s₁ ρ₁ ρ₂} joinForKey s₁ result ⟧ᵛ ρ₁ ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ variablesAt s₁ result ⟧ᵛ ρ₂
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ =
let
-- I'd use rewrite, but Agda gets a memory overflow (?!).
⟦joinAll-result⟧ρ =
subst (λ vs vs ⟧ᵛ ρ₁)
(sym (variablesAt-joinAll s₁ result))
⟦joinForKey-s₁⟧ρ
⟦analyze-result⟧ρ =
updateAll-matches {sv = joinAll result}
ρ₁,bss⇒ρ ⟦joinAll-result⟧ρ
analyze-result≈result =
≈ᵐ-sym {result} {updateAll (joinAll result)}
result≈analyze-result
analyze-s₁≈s₁ =
variablesAt-≈ s₁ (updateAll (joinAll result))
result (analyze-result≈result)
in
⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ
walkTrace : {s₁ s₂ ρ₁ ρ₂} joinForKey s₁ result ⟧ᵛ ρ₁ Trace {graph} s₁ s₂ ρ₁ ρ₂ variablesAt s₂ result ⟧ᵛ ρ₂
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ (Trace-single ρ₁,bss⇒ρ) =
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ
walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
let
⟦result-s₁⟧ρ =
stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ
s₁∈incomingStates =
[]-∈ result (edge⇒incoming s₁→s₂)
(variablesAt-∈ s₁ result)
⟦joinForKey-s⟧ρ =
⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
in
walkTrace ⟦joinForKey-s⟧ρ tr
postulate initialState-pred-∅ : incoming initialState []
joinForKey-initialState-⊥ᵛ : joinForKey initialState result ⊥ᵛ
joinForKey-initialState-⊥ᵛ = cong (λ ins foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
⟦joinAll-initialState⟧ᵛ∅ : joinForKey initialState result ⟧ᵛ []
⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
analyze-correct : {ρ : Env} [] , rootStmt ⇒ˢ ρ variablesAt finalState result ⟧ᵛ ρ
analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)