From 44f04e402068f8cf89ba6b205572d62498fb1742 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 13 Apr 2024 14:08:40 -0700 Subject: [PATCH] Get forward analysis working again Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 40 ++++++++++++++++++++++++---------------- Language.agda | 6 +++--- Lattice.agda | 15 +++++++++++++++ 3 files changed, 42 insertions(+), 19 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index f57e5ba..cf9aa1a 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -145,25 +145,33 @@ module WithProg (prog : Program) where -- 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₂ + 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 s sv = + let + bss = code s + (vs , s,vs∈sv) = locateᵐ {s} {sv} (states-in-Map s sv) + in + foldr updateVariablesFromStmt vs bss 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₂ + updateVariablesForState-Monoʳ s {sv₁} {sv₂} sv₁≼sv₂ = + let + bss = code s + (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 + foldr-Mono' (IsLattice.joinSemilattice isLatticeᵛ) bss + updateVariablesFromStmt updateVariablesFromStmt-Monoʳ + vs₁≼vs₂ open StateVariablesFiniteMap.GeneralizedUpdate states isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states renaming diff --git a/Language.agda b/Language.agda index 66fbcf9..d6aa45c 100644 --- a/Language.agda +++ b/Language.agda @@ -499,10 +499,10 @@ record Program : Set where open Graphs field - prog : Stmt + rootStmt : Stmt private - buildResult = Construction.buildCfg prog empty + buildResult = Construction.buildCfg rootStmt empty graph : Graph graph = proj₁ buildResult @@ -518,7 +518,7 @@ record Program : Set where private vars-Set : StringSet - vars-Set = Stmt-vars prog + vars-Set = Stmt-vars rootStmt vars : List String vars = to-Listˢ vars-Set diff --git a/Lattice.agda b/Lattice.agda index d51e919..dc170cf 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -150,6 +150,21 @@ module _ {a b} {A : Set a} {B : Set b} ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y) (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂)) +module _ {a b} {A : Set a} {B : Set b} + {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B} + (lB : IsSemilattice B _≈₂_ _⊔₂_) where + + open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans) + + open import Data.List as List using (List; foldr; _∷_) + open import Utils using (Pairwise; _∷_) + + foldr-Mono' : ∀ (l : List A) (f : A → B → B) → + (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) → + Monotonic _≼₂_ _≼₂_ (λ b → foldr f b l) + foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂ + foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂) + record IsLattice {a} (A : Set a) (_≈_ : A → A → Set a) (_⊔_ : A → A → A)