diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 5d0458a..a77f30c 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -38,6 +38,8 @@ module WithProg (prog : Program) where -- The variable -> abstract value (e.g. sign) map is a finite value-map -- 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 open VariableValuesFiniteMap using () @@ -96,7 +98,6 @@ module WithProg (prog : Program) where ; ≈₂-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 @@ -150,6 +151,7 @@ module WithProg (prog : Program) where -- 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 + using () renaming ( f' to joinAll ; 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)) = 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. - module WithEvaluator (eval : Expr → VariableValues → L) - (eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e)) where + module _ {{evaluator : Evaluator}} where + open Evaluator evaluator -- 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 + 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 ∷ []) + using () renaming ( f' to updateVariablesFromExpression ; f'-Monotonic to updateVariablesFromExpression-Mono @@ -213,11 +221,13 @@ module WithProg (prog : Program) where vs₁≼vs₂ open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states + using () renaming ( f' to updateAll ; f'-Monotonic to updateAll-Mono ; f'-k∈ks-≡ to updateAll-k∈ks-≡ ) + public -- Finally, the whole analysis consists of getting the 'join' -- 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)) = 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 ⟦⟧ˡ-⊔ˡ-∨ - ) + module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where + open LatticeInterpretation latticeInterpretationˡ + using () + renaming + ( ⟦_⟧ to ⟦_⟧ˡ + ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ + ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨ + ) + public - ⟦_⟧ᵛ : VariableValues → Env → Set - ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v + ⟦_⟧ᵛ : 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∈ρ = + ⟦⟧ᵛ-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')) + + 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 - (l' , (l≈l' , k,l'∈m₁)) = m₂⊆m₁ _ _ k,l∈m₂ - ⟦l'⟧v = ⟦vs₁⟧ρ k,l'∈m₁ k,v∈ρ + 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 - ⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v + ⟦vs⟧ρ₁ k',l∈vs k',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∈ρ)) + 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⟧ρ₁) - ⟦⟧ᵛ-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')) + updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ + updateVariablesForState-matches = + updateVariablesFromStmt-fold-matches - 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⟧ρ₁ + 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⟧ρ₂ + 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 + 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 - joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ - joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅ + 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-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅ + ⟦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⇒ρ) + analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ + analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 636d96e..66b8fc7 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -159,19 +159,20 @@ s₁≢s₂⇒¬s₁∧s₂ { - } { - } +≢+ _ = ⊥-elim (+≢+ refl) ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊥ᵍ} x (_ , bot) = bot ⟦⟧ᵍ-⊓ᵍ-∧ {[ g₁ ]ᵍ} {⊤ᵍ} x (px₁ , _) = px₁ -latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ -latticeInterpretationᵍ = record - { ⟦_⟧ = ⟦_⟧ᵍ - ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ - ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨ - ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧ - } +instance + latticeInterpretationᵍ : LatticeInterpretation isLatticeᵍ + latticeInterpretationᵍ = record + { ⟦_⟧ = ⟦_⟧ᵍ + ; ⟦⟧-respects-≈ = ⟦⟧ᵍ-respects-≈ᵍ + ; ⟦⟧-⊔-∨ = ⟦⟧ᵍ-⊔ᵍ-∨ + ; ⟦⟧-⊓-∧ = ⟦⟧ᵍ-⊓ᵍ-∧ + } module WithProg (prog : Program) where open Program 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₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) @@ -222,15 +223,13 @@ module WithProg (prog : Program) where eval-Mono (# 0) _ = ≈ᵍ-refl eval-Mono (# (suc n')) _ = ≈ᵍ-refl - module ForwardWithEval = ForwardWithProg.WithEvaluator eval eval-Mono - open ForwardWithEval using (result) + instance + SignEval : Evaluator + SignEval = record { eval = eval; eval-Mono = eval-Mono } -- For debugging purposes, print out the 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. -- But agda only simplifies on first argument, apparently, so we are stuck -- listing them all. @@ -281,16 +280,16 @@ module WithProg (prog : Program) where minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt - eval-Valid : InterpretationValid - eval-Valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,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⟧ρ = - minus-valid (eval-Valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-Valid ρ,e₂⇒z₂ ⟦vs⟧ρ) - eval-Valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ + eval-valid : IsValid + eval-valid (⇒ᵉ-+ ρ e₁ e₂ z₁ z₂ ρ,e₁⇒z₁ ρ,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⟧ρ = + minus-valid (eval-valid ρ,e₁⇒z₁ ⟦vs⟧ρ) (eval-valid ρ,e₂⇒z₂ ⟦vs⟧ρ) + eval-valid {vs} (⇒ᵉ-Var ρ x v x,v∈ρ) ⟦vs⟧ρ with ∈k-decᵛ x (proj₁ (proj₁ vs)) ... | yes x∈kvs = ⟦vs⟧ρ (proj₂ (locateᵛ {x} {vs} x∈kvs)) x,v∈ρ ... | no x∉kvs = tt - eval-Valid (⇒ᵉ-ℕ ρ 0) _ = refl - eval-Valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl) + eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl + eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl) - open ForwardWithInterp.WithValidity eval-Valid using (analyze-correct) public + analyze-correct = ForwardWithProg.analyze-correct