diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda new file mode 100644 index 0000000..d8c86bc --- /dev/null +++ b/Analysis/Forward.agda @@ -0,0 +1,187 @@ +open import Language +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.String using (String) renaming (_≟_ to _≟ˢ_) +open import Data.Nat using (suc) +open import Data.Product using (_×_; proj₁; _,_) +open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith) +open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Data.Unit using (⊤) +open import Function using (_∘_) + +open import Utils using (Pairwise) +import Lattice.FiniteValueMap + +open IsFiniteHeightLattice isFiniteHeightLatticeˡ + using () + renaming + ( isLattice to isLatticeˡ + ; fixedHeight to fixedHeightˡ + ; _≼_ to _≼ˡ_ + ) + +module WithProg (prog : Program) where + open Program prog + + -- The variable -> 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.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ + using () + renaming + ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ + ) + + ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec + joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ + fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ + ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ)) + + -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in. + module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states + open StateVariablesFiniteMap + using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks]) + renaming + ( FiniteMap to StateVariables + ; isLattice to isLatticeᵐ + ; _∈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ᵐ + ) + + ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec + fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ + + -- 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 + ) + + -- 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 + ) + public + + states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv + states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s + + -- 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. + + updateVariablesForState : State → StateVariables → VariableValues + updateVariablesForState s sv + with code s + ... | k ← e = + let + (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) + in + updateVariablesFromExpression k e vs + + updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) + updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ + with code s + ... | k ← e = + let + (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 + updateVariablesFromExpression-Mono k e {vs₁} {vs₂} 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 + ) + + -- Finally, the whole sign 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) + public diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 3ebdee6..5567feb 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -1,21 +1,16 @@ module Analysis.Sign where -open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.Nat using (suc) -open import Data.Product using (_×_; proj₁; _,_) +open import Data.Product using (proj₁; _,_) open import Data.Empty using (⊥; ⊥-elim) -open import Data.List using (List; _∷_; []; foldr; cartesianProduct; cartesianProductWith) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) -open import Relation.Nullary using (¬_; Dec; yes; no) -open import Data.Unit using (⊤) -open import Function using (_∘_) +open import Relation.Nullary using (yes; no) open import Language open import Lattice -open import Utils using (Pairwise) open import Showable using (Showable; show) -import Lattice.FiniteValueMap +import Analysis.Forward data Sign : Set where + : Sign @@ -114,101 +109,10 @@ postulate minus-Monoʳ : ∀ (s₁ : SignLattice) → Monotonic _≼ᵍ_ _≼ᵍ module WithProg (prog : Program) where open Program prog - -- The variable -> sign map is a finite value-map with keys strings. Use a bundle to avoid explicitly specifying operators. - module VariableSignsFiniteMap = Lattice.FiniteValueMap.WithKeys _≟ˢ_ isLatticeᵍ vars - open VariableSignsFiniteMap - using () - renaming - ( FiniteMap to VariableSigns - ; 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]ᵛ - ; all-equal-keys to all-equal-keysᵛ - ; ∈k-dec to ∈k-decᵛ - ) - open IsLattice isLatticeᵛ - using () - renaming - ( ⊔-Monotonicˡ to ⊔ᵛ-Monotonicˡ - ; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ - ; ⊔-idemp to ⊔ᵛ-idemp - ) - open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeᵍ vars-Unique ≈ᵍ-dec _ fixedHeightᵍ - using () - renaming - ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ - ) + module ForwardWithProg = Analysis.Forward.WithProg (record { isLattice = isLatticeᵍ; fixedHeight = fixedHeightᵍ }) ≈ᵍ-dec prog + open ForwardWithProg - ≈ᵛ-dec = ≈ᵍ-dec⇒≈ᵛ-dec ≈ᵍ-dec - joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ - fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ - ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ)) - - -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in. - module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states - open StateVariablesFiniteMap - using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks]) - renaming - ( FiniteMap to StateVariables - ; isLattice to isLatticeᵐ - ; _∈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ᵐ - ) - - ≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec - fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ - - -- 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 → VariableSigns - 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 - ) - - -- With 'join' in hand, we need to perform abstract evaluation. - - vars-in-Map : ∀ (k : String) (vs : VariableSigns) → - k ∈ˡ vars → k ∈kᵛ vs - vars-in-Map k vs@(m , kvs≡vars) k∈vars rewrite kvs≡vars = k∈vars - - states-in-Map : ∀ (s : State) (sv : StateVariables) → s ∈kᵐ sv - states-in-Map s sv@(m , ksv≡states) rewrite ksv≡states = states-complete s - - eval : ∀ (e : Expr) → VariableSigns → SignLattice + eval : ∀ (e : Expr) → VariableValues → SignLattice eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) eval (e₁ - e₂) vs = minus (eval e₁ vs) (eval e₂ vs) eval (` k) vs @@ -257,50 +161,7 @@ module WithProg (prog : Program) where eval-Mono (# 0) _ = ≈ᵍ-refl eval-Mono (# (suc n')) _ = ≈ᵍ-refl - private module _ (k : String) (e : Expr) where - open VariableSignsFiniteMap.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 - ) - public + open ForwardWithProg.WithEvaluator eval eval-Mono using (result) - updateVariablesForState : State → StateVariables → VariableSigns - updateVariablesForState s sv - with code s - ... | k ← e = - let - (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) - in - updateVariablesFromExpression k e vs - - updateVariablesForState-Monoʳ : ∀ (s : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (updateVariablesForState s) - updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ - with code s - ... | k ← e = - let - (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 - updateVariablesFromExpression-Mono k e {vs₁} {vs₂} 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 - ) - - 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₂) - - open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂) - using () - renaming (aᶠ to signs) - - - -- Debugging code: print the resulting map. - output = show signs + -- For debugging purposes, print out the result. + output = show result