diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 9702bf9..fd04f0f 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -8,208 +8,28 @@ module Analysis.Forward (≈ˡ-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.String using (String) +open import Data.Product using (_,_) +open import Data.List using (_∷_; []; foldr; foldl) 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 Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; subst) +open import Relation.Nullary using (yes; no) 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 - ) + using () renaming (isLattice to isLatticeˡ) module WithProg (prog : Program) where + open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog + open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog 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. - -- 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 () - 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 - ) - - private - ≈ᵛ-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]ᵐ - ) - open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ - using () - renaming - ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ - ) - open IsFiniteHeightLattice isFiniteHeightLatticeᵐ - using () - renaming - ( ≈-sym to ≈ᵐ-sym - ) - - private - ≈ᵐ-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 - using () - renaming - ( f' to joinAll - ; f'-Monotonic to joinAll-Mono - ; f'-k∈ks-≡ to joinAll-k∈ks-≡ - ) - - private - 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 - - 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. - private module WithEvaluator {{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. - - 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 - ; 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₂ + private module WithStmtEvaluator {{evaluator : StmtEvaluator}} where + open StmtEvaluator evaluator updateVariablesForState : State → StateVariables → VariableValues updateVariablesForState s sv = - foldl (flip updateVariablesFromStmt) (variablesAt s sv) (code s) + foldl (flip (eval s)) (variablesAt s sv) (code s) updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ = @@ -220,7 +40,7 @@ module WithProg (prog : Program) where 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ʳ + (flip (eval s)) (eval-Monoʳ s) vs₁≼vs₂ open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states @@ -256,146 +76,68 @@ 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 - open WithEvaluator - open WithEvaluator using (result; analyze; result≈analyze-result) public + module WithValidInterpretation {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} + {{validEvaluator : ValidStmtEvaluator evaluator latticeInterpretationˡ}} where + open ValidStmtEvaluator validEvaluator - private module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} where - open LatticeInterpretation latticeInterpretationˡ - using () - renaming - ( ⟦_⟧ to ⟦_⟧ˡ - ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ - ; ⟦⟧-⊔-∨ to ⟦⟧ˡ-⊔ˡ-∨ - ) - public + eval-fold-valid : ∀ {s bss vs ρ₁ ρ₂} → ρ₁ , bss ⇒ᵇˢ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ foldl (flip (eval s)) vs bss ⟧ᵛ ρ₂ + eval-fold-valid {_} [] ⟦vs⟧ρ = ⟦vs⟧ρ + eval-fold-valid {s} {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ = + eval-fold-valid + {bss = bss'} {eval s bs vs} ρ,bss'⇒ρ₂ + (valid ρ₁,bs⇒ρ ⟦vs⟧ρ₁) - ⟦_⟧ᵛ : VariableValues → Env → Set - ⟦_⟧ᵛ vs ρ = ∀ {k l} → (k , l) ∈ᵛ vs → ∀ {v} → (k , v) Language.∈ ρ → ⟦ l ⟧ˡ v + updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ + updateVariablesForState-matches = eval-fold-valid - ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ [] - ⟦⊥ᵛ⟧ᵛ∅ _ () + 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⟧ρ₁ - ⟦⟧ᵛ-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 + 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⟧ρ₂ - ⟦⟧ᵛ-⊔ᵛ-∨ : ∀ {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 public - open LatticeInterpretation interpretation public - - field - valid : IsValid - - module WithValidInterpretation {{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'∈ρ₁ = + 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 - k'∉[k] = (λ { (Any.here refl) → k≢k' refl }) - k',l∈vs = updateVariablesFromExpression-k∉ks-backward k e {l = vs} k'∉[k] k',l∈vs' + ⟦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 - ⟦vs⟧ρ₁ k',l∈vs k',v'∈ρ₁ + walkTrace ⟦joinForKey-s⟧ρ tr - 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⟧ρ₁) + joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ + joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅ - updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ - updateVariablesForState-matches = - updateVariablesFromStmt-fold-matches + ⟦joinAll-initialState⟧ᵛ∅ : ⟦ joinForKey initialState result ⟧ᵛ [] + ⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs → ⟦ vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅ - 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⟧ρ₁ + analyze-correct : ∀ {ρ : Env} → [] , rootStmt ⇒ˢ ρ → ⟦ variablesAt finalState result ⟧ᵛ ρ + analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ) - - 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 - - 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⇒ρ) - - open WithValidInterpretation using (analyze-correct) public + open WithStmtEvaluator using (result; analyze; result≈analyze-result) public + open WithStmtEvaluator.WithValidInterpretation using (analyze-correct) public diff --git a/Analysis/Forward/Adapters.agda b/Analysis/Forward/Adapters.agda new file mode 100644 index 0000000..01b6ba7 --- /dev/null +++ b/Analysis/Forward/Adapters.agda @@ -0,0 +1,100 @@ +open import Language hiding (_[_]) +open import Lattice + +module Analysis.Forward.Adapters + {L : Set} {h} + {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} + (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) + (≈ˡ-dec : IsDecidable _≈ˡ_) + (prog : Program) where + +open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog +open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog + +open import Data.Empty using (⊥-elim) +open import Data.String using (String) renaming (_≟_ to _≟ˢ_) +open import Data.Product using (_,_) +open import Data.List using (_∷_; []; foldr; foldl) +open import Data.List.Relation.Unary.Any as Any using () +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; subst) +open import Relation.Nullary using (yes; no) +open import Function using (_∘_; flip) + +open IsFiniteHeightLattice isFiniteHeightLatticeˡ + using () + renaming + ( isLattice to isLatticeˡ + ; _≼_ to _≼ˡ_ + ) +open Program prog + +-- Now, allow StmtEvaluators to be auto-constructed from ExprEvaluators. +module ExprToStmtAdapter {{ exprEvaluator : ExprEvaluator }} where + open ExprEvaluator exprEvaluator + using () + renaming + ( eval to evalᵉ + ; eval-Monoʳ to evalᵉ-Monoʳ + ) + + -- 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 ∷ []) + using () + 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. + + evalᵇ : State → BasicStmt → VariableValues → VariableValues + evalᵇ _ (k ← e) vs = updateVariablesFromExpression k e vs + evalᵇ _ noop vs = vs + + evalᵇ-Monoʳ : ∀ (s : State) (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (evalᵇ s bs) + evalᵇ-Monoʳ _ (k ← e) {vs₁} {vs₂} vs₁≼vs₂ = updateVariablesFromExpression-Mono k e {vs₁} {vs₂} vs₁≼vs₂ + evalᵇ-Monoʳ _ noop vs₁≼vs₂ = vs₁≼vs₂ + + instance + stmtEvaluator : StmtEvaluator + stmtEvaluator = record { eval = evalᵇ ; eval-Monoʳ = evalᵇ-Monoʳ } + + -- Moreover, correct StmtEvaluators can be constructed from correct + -- ExprEvaluators. + module _ {{latticeInterpretationˡ : LatticeInterpretation isLatticeˡ}} + {{isValid : ValidExprEvaluator exprEvaluator latticeInterpretationˡ}} where + open ValidExprEvaluator isValid using () renaming (valid to validᵉ) + + evalᵇ-valid : ∀ {s vs ρ₁ ρ₂ bs} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ evalᵇ s bs vs ⟧ᵛ ρ₂ + evalᵇ-valid {_} {vs} {ρ₁} {ρ₁} {_} (⇒ᵇ-noop ρ₁) ⟦vs⟧ρ₁ = ⟦vs⟧ρ₁ + evalᵇ-valid {_} {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 + 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'∈ρ₁ + + instance + validStmtEvaluator : ValidStmtEvaluator stmtEvaluator latticeInterpretationˡ + validStmtEvaluator = record + { valid = λ {a} {b} {c} {d} → evalᵇ-valid {a} {b} {c} {d} + } diff --git a/Analysis/Forward/Evaluation.agda b/Analysis/Forward/Evaluation.agda new file mode 100644 index 0000000..acd681a --- /dev/null +++ b/Analysis/Forward/Evaluation.agda @@ -0,0 +1,66 @@ +open import Language hiding (_[_]) +open import Lattice + +module Analysis.Forward.Evaluation + {L : Set} {h} + {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} + (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) + (≈ˡ-dec : IsDecidable _≈ˡ_) + (prog : Program) where + +open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog +open import Data.Product using (_,_) + +open IsFiniteHeightLattice isFiniteHeightLatticeˡ + using () + renaming + ( isLattice to isLatticeˡ + ; _≼_ to _≼ˡ_ + ) +open Program prog + +-- The "full" version of the analysis ought to define a function +-- that analyzes each basic statement. For some analyses, the state ID +-- is used as part of the lattice, so include it here. +record StmtEvaluator : Set where + field + eval : State → BasicStmt → VariableValues → VariableValues + eval-Monoʳ : ∀ (s : State) (bs : BasicStmt) → Monotonic _≼ᵛ_ _≼ᵛ_ (eval s bs) + +-- For some "simpler" analyes, all we need to do is analyze the expressions. +-- For that purpose, provide a simpler evaluator type. +record ExprEvaluator : Set where + field + eval : Expr → VariableValues → L + eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ˡ_ (eval e) + +-- Evaluators have a notion of being "valid", in which the (symbolic) +-- manipulations on lattice elements they perform match up with +-- the semantics. Define what it means to be valid for statement and +-- expression-based evaluators. Define "IsValidExprEvaluator" +-- and "IsValidStmtEvaluator" standalone so that users can use them +-- in their type expressions. + +module _ {{evaluator : ExprEvaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where + open ExprEvaluator evaluator + open LatticeInterpretation interpretation + + IsValidExprEvaluator : Set + IsValidExprEvaluator = ∀ {vs ρ e v} → ρ , e ⇒ᵉ v → ⟦ vs ⟧ᵛ ρ → ⟦ eval e vs ⟧ˡ v + +record ValidExprEvaluator (evaluator : ExprEvaluator) + (interpretation : LatticeInterpretation isLatticeˡ) : Set₁ where + field + valid : IsValidExprEvaluator {{evaluator}} {{interpretation}} + +module _ {{evaluator : StmtEvaluator}} {{interpretation : LatticeInterpretation isLatticeˡ}} where + open StmtEvaluator evaluator + open LatticeInterpretation interpretation + + IsValidStmtEvaluator : Set + IsValidStmtEvaluator = ∀ {s vs ρ₁ ρ₂ bs} → ρ₁ , bs ⇒ᵇ ρ₂ → ⟦ vs ⟧ᵛ ρ₁ → ⟦ eval s bs vs ⟧ᵛ ρ₂ + +record ValidStmtEvaluator (evaluator : StmtEvaluator) + (interpretation : LatticeInterpretation isLatticeˡ) : Set₁ where + field + valid : IsValidStmtEvaluator {{evaluator}} {{interpretation}} diff --git a/Analysis/Forward/Lattices.agda b/Analysis/Forward/Lattices.agda new file mode 100644 index 0000000..7becec0 --- /dev/null +++ b/Analysis/Forward/Lattices.agda @@ -0,0 +1,211 @@ +open import Language hiding (_[_]) +open import Lattice + +module Analysis.Forward.Lattices + {L : Set} {h} + {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} + (isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) + (≈ˡ-dec : IsDecidable _≈ˡ_) + (prog : Program) where + +open import Data.String using () renaming (_≟_ to _≟ˢ_) +open import Data.Product using (proj₁; proj₂; _,_) +open import Data.Sum using (inj₁; inj₂) +open import Data.List using (List; _∷_; []; foldr) +open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) +open import Data.List.Relation.Unary.Any as Any using () +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Utils using (Pairwise; _⇒_; _∨_) + +open IsFiniteHeightLattice isFiniteHeightLatticeˡ + using () + renaming + ( isLattice to isLatticeˡ + ; fixedHeight to fixedHeightˡ + ; ≈-sym to ≈ˡ-sym + ) +open Program prog + +import Lattice.FiniteValueMap +import Chain + +-- 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 () + 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 + ) + public +open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ + using () + renaming + ( Provenance-union to Provenance-unionᵐ + ) + public +open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ + using () + renaming + ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ + ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms + ) + public + +≈ᵛ-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ᵐ + ) + public +open IsFiniteHeightLattice isFiniteHeightLatticeᵐ + using () + renaming + ( ≈-sym to ≈ᵐ-sym + ) + public + +≈ᵐ-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 + using () + renaming + ( f' to joinAll + ; f'-Monotonic to joinAll-Mono + ; f'-k∈ks-≡ to joinAll-k∈ks-≡ + ) + public + +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 + +-- Elements of the lattice type L describe individual variables. What +-- exactly each lattice element says about the variable is defined +-- by a LatticeInterpretation element. We've now constructed the +-- (Variable → L) lattice, which describes states, and we need to lift +-- the "meaning" of the element lattice to a descriptions of states. +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 + + ⟦⊥ᵛ⟧ᵛ∅ : ⟦ ⊥ᵛ ⟧ᵛ [] + ⟦⊥ᵛ⟧ᵛ∅ _ () + + ⟦⟧ᵛ-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')) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 66b8fc7..7f80427 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -62,7 +62,7 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s open AB.Plain 0ˢ using () renaming ( isLattice to isLatticeᵍ - ; fixedHeight to fixedHeightᵍ + ; isFiniteHeightLattice to isFiniteHeightLatticeᵍ ; _≼_ to _≼ᵍ_ ; _⊔_ to _⊔ᵍ_ ; _⊓_ to _⊓ᵍ_ @@ -171,8 +171,9 @@ instance module WithProg (prog : Program) where open Program prog - module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog - open ForwardWithProg hiding (analyze-correct) + open import Analysis.Forward.Lattices isFiniteHeightLatticeᵍ ≈ᵍ-dec prog + open import Analysis.Forward.Evaluation isFiniteHeightLatticeᵍ ≈ᵍ-dec prog + open import Analysis.Forward.Adapters isFiniteHeightLatticeᵍ ≈ᵍ-dec prog eval : ∀ (e : Expr) → VariableValues → SignLattice eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) @@ -184,8 +185,8 @@ module WithProg (prog : Program) where eval (# 0) _ = [ 0ˢ ]ᵍ eval (# (suc n')) _ = [ + ]ᵍ - eval-Mono : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e) - eval-Mono (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ = + eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᵍ_ (eval e) + eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ = let -- TODO: can this be done with less boilerplate? g₁vs₁ = eval e₁ vs₁ @@ -195,9 +196,9 @@ module WithProg (prog : Program) where in ≼ᵍ-trans {plus g₁vs₁ g₂vs₁} {plus g₁vs₂ g₂vs₁} {plus g₁vs₂ g₂vs₂} - (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ {vs₁} {vs₂} vs₁≼vs₂)) - (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂)) - eval-Mono (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ = + (plus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Monoʳ e₁ {vs₁} {vs₂} vs₁≼vs₂)) + (plus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Monoʳ e₂ {vs₁} {vs₂} vs₁≼vs₂)) + eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ = let -- TODO: here too -- can this be done with less boilerplate? g₁vs₁ = eval e₁ vs₁ @@ -207,9 +208,9 @@ module WithProg (prog : Program) where in ≼ᵍ-trans {minus g₁vs₁ g₂vs₁} {minus g₁vs₂ g₂vs₁} {minus g₁vs₂ g₂vs₂} - (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Mono e₁ {vs₁} {vs₂} vs₁≼vs₂)) - (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Mono e₂ {vs₁} {vs₂} vs₁≼vs₂)) - eval-Mono (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂ + (minus-Monoˡ g₂vs₁ {g₁vs₁} {g₁vs₂} (eval-Monoʳ e₁ {vs₁} {vs₂} vs₁≼vs₂)) + (minus-Monoʳ g₁vs₂ {g₂vs₁} {g₂vs₂} (eval-Monoʳ e₂ {vs₁} {vs₂} vs₁≼vs₂)) + eval-Monoʳ (` k) {vs₁@((kvs₁ , _) , _)} {vs₂@((kvs₂ , _), _)} vs₁≼vs₂ with ∈k-decᵛ k kvs₁ | ∈k-decᵛ k kvs₂ ... | yes k∈kvs₁ | yes k∈kvs₂ = let @@ -220,15 +221,15 @@ module WithProg (prog : Program) where ... | yes k∈kvs₁ | no k∉kvs₂ = ⊥-elim (k∉kvs₂ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₁ vs₂) k∈kvs₁)) ... | no k∉kvs₁ | yes k∈kvs₂ = ⊥-elim (k∉kvs₁ (subst (λ l → k ∈ˡ l) (all-equal-keysᵛ vs₂ vs₁) k∈kvs₂)) ... | no k∉kvs₁ | no k∉kvs₂ = IsLattice.≈-refl isLatticeᵍ - eval-Mono (# 0) _ = ≈ᵍ-refl - eval-Mono (# (suc n')) _ = ≈ᵍ-refl + eval-Monoʳ (# 0) _ = ≈ᵍ-refl + eval-Monoʳ (# (suc n')) _ = ≈ᵍ-refl instance - SignEval : Evaluator - SignEval = record { eval = eval; eval-Mono = eval-Mono } + SignEval : ExprEvaluator + SignEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ } -- For debugging purposes, print out the result. - output = show result + output = show (Analysis.Forward.WithProg.result isFiniteHeightLatticeᵍ ≈ᵍ-dec prog) -- 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 @@ -280,7 +281,7 @@ module WithProg (prog : Program) where minus-valid {[ 0ˢ ]ᵍ} {[ 0ˢ ]ᵍ} refl refl = refl minus-valid {[ 0ˢ ]ᵍ} {⊤ᵍ} _ _ = tt - eval-valid : IsValid + eval-valid : IsValidExprEvaluator 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⟧ρ = @@ -292,4 +293,4 @@ module WithProg (prog : Program) where eval-valid (⇒ᵉ-ℕ ρ 0) _ = refl eval-valid (⇒ᵉ-ℕ ρ (suc n')) _ = (n' , refl) - analyze-correct = ForwardWithProg.analyze-correct + analyze-correct = Analysis.Forward.WithProg.analyze-correct