From 5d56a7ce2d8bf2736704af6e25fc9d885ecf845a Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 23 Mar 2024 12:09:14 -0700 Subject: [PATCH] Fix comments in Forward.agda Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index d8c86bc..f57e5ba 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -31,7 +31,8 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ 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. + -- 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 () @@ -69,7 +70,7 @@ module WithProg (prog : Program) where fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ)) - -- Finally, the map we care about is (state -> (variables -> sign)). Bring that in. + -- 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]) @@ -170,7 +171,7 @@ module WithProg (prog : Program) where ; f'-Monotonic to updateAll-Mono ) - -- Finally, the whole sign 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 -- function. This is just a composition, and is trivially monotonic. @@ -178,7 +179,9 @@ module WithProg (prog : Program) where 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₂) + 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₂)