DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Use instance search to avoid multiply-nested modules

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2024-12-31 00:21:10 -08:00
parent 9131214880
commit 10332351ea
2 changed files with 159 additions and 133 deletions
Download Patch File Download Diff File Expand all files Collapse all files

249
Analysis/Forward.agda
View File

@@ -38,6 +38,8 @@ module WithProg (prog : Program) where
-- The variable -> abstract value (e.g. sign) map is a finite value-map -- The variable -> abstract value (e.g. sign) map is a finite value-map
-- with keys strings. Use a bundle to avoid explicitly specifying operators. -- with keys strings. Use a bundle to avoid explicitly specifying operators.
-- It's helpful to export these via 'public' since consumers tend to
-- use various variable lattice operations.
module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars module VariableValuesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeˡ vars
open VariableValuesFiniteMap open VariableValuesFiniteMap
using () using ()
@@ -96,7 +98,6 @@ module WithProg (prog : Program) where
; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec ; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
) )
public
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ
using () using ()
renaming renaming
@@ -150,6 +151,7 @@ module WithProg (prog : Program) where
-- The name f' comes from the formulation of Exercise 4.26. -- 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 open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
using ()
renaming renaming
( f' to joinAll ( f' to joinAll
; f'-Monotonic to joinAll-Mono ; f'-Monotonic to joinAll-Mono
@@ -162,16 +164,22 @@ module WithProg (prog : Program) where
with (vs , s,vs∈usv) ← locateᵐ {s} {joinAll sv} (states-in-Map s (joinAll 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 joinAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
record Evaluator : Set where
field
eval : Expr → VariableValues → L
eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)
-- With 'join' in hand, we need to perform abstract evaluation. -- With 'join' in hand, we need to perform abstract evaluation.
module WithEvaluator (eval : Expr → VariableValues → L) module _ {{evaluator : Evaluator}} where
(eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where open Evaluator evaluator
-- For a particular evaluation function, we need to perform an evaluation -- For a particular evaluation function, we need to perform an evaluation
-- for an assignment, and update the corresponding key. Use Exercise 4.26's -- for an assignment, and update the corresponding key. Use Exercise 4.26's
-- generalized update to set the single key's value. -- generalized update to set the single key's value.
private module _ (k : String) (e : Expr) where 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 ∷ []) 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 ∷ [])
using ()
renaming renaming
( f' to updateVariablesFromExpression ( f' to updateVariablesFromExpression
; f'-Monotonic to updateVariablesFromExpression-Mono ; f'-Monotonic to updateVariablesFromExpression-Mono
@@ -213,11 +221,13 @@ module WithProg (prog : Program) where
vs₁≼vs₂ vs₁≼vs₂
open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
using ()
renaming renaming
( f' to updateAll ( f' to updateAll
; f'-Monotonic to updateAll-Mono ; f'-Monotonic to updateAll-Mono
; f'-k∈ks-≡ to updateAll-k∈ks-≡ ; f'-k∈ks-≡ to updateAll-k∈ks-≡
) )
public
-- Finally, the whole analysis consists of getting the 'join' -- Finally, the whole analysis consists of getting the 'join'
-- of all incoming states, then applying the per-state evaluation -- of all incoming states, then applying the per-state evaluation
@@ -243,124 +253,141 @@ module WithProg (prog : Program) where
with (vs , s,vs∈usv) ← locateᵐ {s} {updateAll sv} (states-in-Map s (updateAll 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 updateAll-k∈ks-≡ {l = sv} (states-complete s) s,vs∈usv
module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where
open LatticeInterpretation latticeInterpretationˡ open LatticeInterpretation latticeInterpretationˡ
using () using ()
renaming renaming
( ⟦_⟧ to ⟦_⟧ˡ ( ⟦_⟧ to ⟦_⟧ˡ
; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨ ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨
) )
public
⟦_⟧ᵛ : VariableValues → Env → Set ⟦_⟧ᵛ : VariableValues → Env → Set
⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v
⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ [] ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ []
⟦⊥ᵛ⟧ᵛ∅ _ () ⟦⊥ᵛ⟧ᵛ∅ _ ()
⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ ⟦⟧ᵛ-respects-≈ᵛ : ∀ {vs₁ vs₂ : VariableValues} → vs₁ ≈ᵛ vs₂ → ⟦ vs₁ ⟧ᵛ ⇒ ⟦ vs₂ ⟧ᵛ
⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _} ⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
(m₁⊆m₂ , m₂⊆m₁) ρ ⟦vs₁⟧ρ {k} {l} k,l∈m₂ {v} k,v∈ρ = (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'))
module _ {{evaluator : Evaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where
open Evaluator evaluator
open LatticeInterpretation interpretation
IsValid : Set
IsValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v
record ValidInterpretation : Set₁ where
field
{{evaluator}} : Evaluator
{{interpretation}} : LatticeInterpretation isLatticeˡ
open Evaluator evaluator
open LatticeInterpretation interpretation
field
valid : IsValid
module _ {{validInterpretation : ValidInterpretation}} where
open ValidInterpretation validInterpretation
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' =
valid ρ,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 let
(l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂ k'∉[k] = (λ { (Any.here refl) → k≢k' refl })
⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs'
in in
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁
⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {vs₁ vs₂ : VariableValues} → (⟦ vs₁ ⟧ᵛ ∨ ⟦ vs₂ ⟧ᵛ) ⇒ ⟦ vs₁ ⊔ᵛ vs₂ ⟧ᵛ updateVariablesFromStmt-fold-matches : ∀ {bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
⟦⟧ᵛ-⊔ᵛ-∨ {vs₁} {vs₂} ρ ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂))) updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ =
← Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂ updateVariablesFromStmt-fold-matches
with ⟦vs₁⟧ρ∨⟦vs₂⟧ρ {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
... | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ)) (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁)
... | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ-∨ {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
⟦⟧ᵛ-foldr : ∀ {vs : VariableValues} {vss : List VariableValues} {ρ : Env} → updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂
⟦ vs ⟧ᵛ ρ → vs ∈ˡ vss → ⟦ foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ updateVariablesForState-matches =
⟦⟧ᵛ-foldr {vs} {vs ∷ vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) = updateVariablesFromStmt-fold-matches
⟦⟧ᵛ-⊔ᵛ-∨ {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 updateAll-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
InterpretationValid = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v updateAll-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
rewrite variablesAt-updateAll s sv =
module WithValidity (interpretationValidˡ : InterpretationValid) where updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ₂ ⟦vs⟧ρ₁
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₁ result ⟧ᵛ ρ₁ → ρ₁ , (code s₁) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s₁ result ⟧ᵛ ρ₂
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ = stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ =
let let
-- I'd use rewrite, but Agda gets a memory overflow (?!). -- I'd use rewrite, but Agda gets a memory overflow (?!).
⟦joinAll-result⟧ρ₁ = ⟦joinAll-result⟧ρ₁ =
subst (λ vs → ⟦ vs ⟧ᵛ ρ₁) subst (λ vs → ⟦ vs ⟧ᵛ ρ₁)
(sym (variablesAt-joinAll s₁ result)) (sym (variablesAt-joinAll s₁ result))
⟦joinForKey-s₁⟧ρ₁ ⟦joinForKey-s₁⟧ρ₁
⟦analyze-result⟧ρ₂ = ⟦analyze-result⟧ρ₂ =
updateAll-matches {sv = joinAll result} updateAll-matches {sv = joinAll result}
ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁ ρ₁,bss⇒ρ₂ ⟦joinAll-result⟧ρ₁
analyze-result≈result = analyze-result≈result =
≈ᵐ-sym {result} {updateAll (joinAll result)} ≈ᵐ-sym {result} {updateAll (joinAll result)}
result≈analyze-result result≈analyze-result
analyze-s₁≈s₁ = analyze-s₁≈s₁ =
variablesAt-≈ s₁ (updateAll (joinAll result)) variablesAt-≈ s₁ (updateAll (joinAll result))
result (analyze-result≈result) result (analyze-result≈result)
in in
⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ₂ ⟦⟧ᵛ-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₁ result ⟧ᵛ ρ₁ → Trace {graph} s₁ s₂ ρ₁ ρ₂ → ⟦ variablesAt s₂ result ⟧ᵛ ρ₂
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) = walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-single ρ₁,bss⇒ρ₂) =
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂ stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ₂
walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) = walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ₁ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
let let
⟦result-s₁⟧ρ = ⟦result-s₁⟧ρ =
stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ₁ ρ₁,bss⇒ρ
s₁∈incomingStates = s₁∈incomingStates =
[]-∈ result (edge⇒incoming s₁→s₂) []-∈ result (edge⇒incoming s₁→s₂)
(variablesAt-∈ s₁ result) (variablesAt-∈ s₁ result)
⟦joinForKey-s⟧ρ = ⟦joinForKey-s⟧ρ =
⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates ⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
in in
walkTrace ⟦joinForKey-s⟧ρ tr walkTrace ⟦joinForKey-s⟧ρ tr
joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ
joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅ joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ [] ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ []
⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅ ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ
analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ) analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)

43
Analysis/Sign.agda
View File

@@ -159,19 +159,20 @@ s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl)
⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot
⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁ ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁
latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ instance
latticeInterpretationᵍ = record latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ
{ ⟦_⟧ = ⟦_⟧ᵍ latticeInterpretationᵍ = record
; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ { ⟦_⟧ = ⟦_⟧ᵍ
; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨ ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ
; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧ ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨
} ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧
}
module WithProg (prog : Program) where module WithProg (prog : Program) where
open Program prog open Program prog
module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog
open ForwardWithProg open ForwardWithProg hiding (analyze-correct)
eval : ∀ (e : Expr) → VariableValues → SignLattice eval : ∀ (e : Expr) → VariableValues → SignLattice
eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
@@ -222,15 +223,13 @@ module WithProg (prog : Program) where
eval-Mono (# 0) _ = ≈ᵍ-refl eval-Mono (# 0) _ = ≈ᵍ-refl
eval-Mono (# (suc n')) _ = ≈ᵍ-refl eval-Mono (# (suc n')) _ = ≈ᵍ-refl
module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono instance
open ForwardWithEval using (result) SignEval : Evaluator
SignEval = record { eval = eval; eval-Mono = eval-Mono }
-- For debugging purposes, print out the result. -- For debugging purposes, print out the result.
output = show result output = show result
module ForwardWithInterp = ForwardWithEval.WithInterpretation latticeInterpretationᵍ
open ForwardWithInterp using (⟦_⟧ᵛ; InterpretationValid)
-- This should have fewer cases -- the same number as the actual 'plus' above. -- This should have fewer cases -- the same number as the actual 'plus' above.
-- But agda only simplifies on first argument, apparently, so we are stuck -- But agda only simplifies on first argument, apparently, so we are stuck
-- listing them all. -- listing them all.
@@ -281,16 +280,16 @@ module WithProg (prog : Program) where
minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl
minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt
eval-Valid : InterpretationValid eval-valid : IsValid
eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ = eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
plus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ) plus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
eval-Valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ = eval-valid (⇒ᵉ-- ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,e₂⇒z₂) ⟦vs⟧ρ =
minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ) minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ)
eval-Valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ
with ∈k-decᵛ x (proj₁ (proj₁ vs)) with ∈k-decᵛ x (proj₁ (proj₁ vs))
... | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ ... | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ
... | no x∉kvs = tt ... | no x∉kvs = tt
eval-Valid (⇒ᵉ-ℕ ρ 0) _ = refl eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl
eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl) eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl)
open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public analyze-correct = ForwardWithProg.analyze-correct