From 33cc0f9fe9a7371a086134fe5020d08f6dae04a0 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 5 Jan 2025 19:38:55 -0800 Subject: [PATCH] Implement constant analysis Signed-off-by: Danila Fedorin --- Analysis/Constant.agda | 223 ++++++++++++++++++++++++++++++++++++++++ Lattice/AboveBelow.agda | 2 +- Main.agda | 11 +- 3 files changed, 231 insertions(+), 5 deletions(-) create mode 100644 Analysis/Constant.agda diff --git a/Analysis/Constant.agda b/Analysis/Constant.agda new file mode 100644 index 0000000..9da3458 --- /dev/null +++ b/Analysis/Constant.agda @@ -0,0 +1,223 @@ + +module Analysis.Constant where + +open import Data.Integer as Int using (ℤ; +_; -[1+_]; _≟_) +open import Data.Integer.Show as IntShow using () +open import Data.Nat as Nat using (ℕ; suc; zero) +open import Data.Product using (Σ; proj₁; proj₂; _,_) +open import Data.Sum using (inj₁; inj₂) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Unit using (⊤; tt) +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 (¬_; yes; no) + +open import Equivalence +open import Language +open import Lattice +open import Showable using (Showable; show) +open import Utils using (_⇒_; _∧_; _∨_) +open import Analysis.Utils using (eval-combine₂) +import Analysis.Forward + +instance + showable : Showable ℤ + showable = record + { show = IntShow.show + } + +instance + ≡-equiv : IsEquivalence ℤ _≡_ + ≡-equiv = record + { ≈-refl = refl + ; ≈-sym = sym + ; ≈-trans = trans + } + + ≡-Decidable-ℤ : IsDecidable {_} {ℤ} _≡_ + ≡-Decidable-ℤ = record { R-dec = _≟_ } + +-- embelish 'ℕ' with a top and bottom element. +open import Lattice.AboveBelow ℤ _ as AB + using () + renaming + ( AboveBelow to ConstLattice + ; ≈-dec to ≈ᶜ-dec + ; ⊥ to ⊥ᶜ + ; ⊤ to ⊤ᶜ + ; [_] to [_]ᶜ + ; _≈_ to _≈ᶜ_ + ; ≈-⊥-⊥ to ≈ᶜ-⊥ᶜ-⊥ᶜ + ; ≈-⊤-⊤ to ≈ᶜ-⊤ᶜ-⊤ᶜ + ; ≈-lift to ≈ᶜ-lift + ; ≈-refl to ≈ᶜ-refl + ) +-- 'ℕ''s structure is not finite, so just use a 'plain' above-below Lattice. +open AB.Plain (+ 0) using () + renaming + ( isLattice to isLatticeᶜ + ; isFiniteHeightLattice to isFiniteHeightLatticeᵍ + ; _≼_ to _≼ᶜ_ + ; _⊔_ to _⊔ᶜ_ + ; _⊓_ to _⊓ᶜ_ + ; ≼-trans to ≼ᶜ-trans + ; ≼-refl to ≼ᶜ-refl + ) + +plus : ConstLattice → ConstLattice → ConstLattice +plus ⊥ᶜ _ = ⊥ᶜ +plus _ ⊥ᶜ = ⊥ᶜ +plus ⊤ᶜ _ = ⊤ᶜ +plus _ ⊤ᶜ = ⊤ᶜ +plus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.+ z₂ ]ᶜ + +-- this is incredibly tedious: 125 cases per monotonicity proof, and tactics +-- are hard. postulate for now. +postulate plus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → plus s₁ s₂) +postulate plus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (plus s₁) + +plus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ plus +plus-Mono₂ = (plus-Monoˡ , plus-Monoʳ) + +minus : ConstLattice → ConstLattice → ConstLattice +minus ⊥ᶜ _ = ⊥ᶜ +minus _ ⊥ᶜ = ⊥ᶜ +minus ⊤ᶜ _ = ⊤ᶜ +minus _ ⊤ᶜ = ⊤ᶜ +minus [ z₁ ]ᶜ [ z₂ ]ᶜ = [ z₁ Int.- z₂ ]ᶜ + +postulate minus-Monoˡ : ∀ (s₂ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (λ s₁ → minus s₁ s₂) +postulate minus-Monoʳ : ∀ (s₁ : ConstLattice) → Monotonic _≼ᶜ_ _≼ᶜ_ (minus s₁) + +minus-Mono₂ : Monotonic₂ _≼ᶜ_ _≼ᶜ_ _≼ᶜ_ minus +minus-Mono₂ = (minus-Monoˡ , minus-Monoʳ) + +⟦_⟧ᶜ : ConstLattice → Value → Set +⟦_⟧ᶜ ⊥ᶜ _ = ⊥ +⟦_⟧ᶜ ⊤ᶜ _ = ⊤ +⟦_⟧ᶜ [ z ]ᶜ v = v ≡ ↑ᶻ z + +⟦⟧ᶜ-respects-≈ᶜ : ∀ {s₁ s₂ : ConstLattice} → s₁ ≈ᶜ s₂ → ⟦ s₁ ⟧ᶜ ⇒ ⟦ s₂ ⟧ᶜ +⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊥ᶜ-⊥ᶜ v bot = bot +⟦⟧ᶜ-respects-≈ᶜ ≈ᶜ-⊤ᶜ-⊤ᶜ v top = top +⟦⟧ᶜ-respects-≈ᶜ (≈ᶜ-lift { z } { z } refl) v proof = proof + +⟦⟧ᶜ-⊔ᶜ-∨ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∨ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊔ᶜ s₂ ⟧ᶜ +⟦⟧ᶜ-⊔ᶜ-∨ {⊥ᶜ} x (inj₂ px₂) = px₂ +⟦⟧ᶜ-⊔ᶜ-∨ {⊤ᶜ} x _ = tt +⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x px + with s₁ ≟ s₂ +... | no _ = tt +... | yes refl + with px +... | inj₁ px₁ = px₁ +... | inj₂ px₂ = px₂ +⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊥ᶜ} x (inj₁ px₁) = px₁ +⟦⟧ᶜ-⊔ᶜ-∨ {[ s₁ ]ᶜ} {⊤ᶜ} x _ = tt + +s₁≢s₂⇒¬s₁∧s₂ : ∀ {z₁ z₂ : ℤ} → ¬ z₁ ≡ z₂ → ∀ {v} → ¬ ((⟦ [ z₁ ]ᶜ ⟧ᶜ ∧ ⟦ [ z₂ ]ᶜ ⟧ᶜ) v) +s₁≢s₂⇒¬s₁∧s₂ { z₁ } { z₂ } z₁≢z₂ {v} (v≡z₁ , v≡z₂) + with refl ← trans (sym v≡z₁) v≡z₂ = z₁≢z₂ refl + +⟦⟧ᶜ-⊓ᶜ-∧ : ∀ {s₁ s₂ : ConstLattice} → (⟦ s₁ ⟧ᶜ ∧ ⟦ s₂ ⟧ᶜ) ⇒ ⟦ s₁ ⊓ᶜ s₂ ⟧ᶜ +⟦⟧ᶜ-⊓ᶜ-∧ {⊥ᶜ} x (bot , _) = bot +⟦⟧ᶜ-⊓ᶜ-∧ {⊤ᶜ} x (_ , px₂) = px₂ +⟦⟧ᶜ-⊓ᶜ-∧ {[ s₁ ]ᶜ} {[ s₂ ]ᶜ} x (px₁ , px₂) + with s₁ ≟ s₂ +... | no s₁≢s₂ = s₁≢s₂⇒¬s₁∧s₂ s₁≢s₂ (px₁ , px₂) +... | yes refl = px₁ +⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊥ᶜ} x (_ , bot) = bot +⟦⟧ᶜ-⊓ᶜ-∧ {[ g₁ ]ᶜ} {⊤ᶜ} x (px₁ , _) = px₁ + +instance + latticeInterpretationᶜ : LatticeInterpretation isLatticeᶜ + latticeInterpretationᶜ = record + { ⟦_⟧ = ⟦_⟧ᶜ + ; ⟦⟧-respects-≈ = ⟦⟧ᶜ-respects-≈ᶜ + ; ⟦⟧-⊔-∨ = ⟦⟧ᶜ-⊔ᶜ-∨ + ; ⟦⟧-⊓-∧ = ⟦⟧ᶜ-⊓ᶜ-∧ + } + +module WithProg (prog : Program) where + open Program prog + + open import Analysis.Forward.Lattices ConstLattice prog + open import Analysis.Forward.Evaluation ConstLattice prog + open import Analysis.Forward.Adapters ConstLattice prog + + eval : ∀ (e : Expr) → VariableValues → ConstLattice + 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 + with ∈k-decᵛ k (proj₁ (proj₁ vs)) + ... | yes k∈vs = proj₁ (locateᵛ {k} {vs} k∈vs) + ... | no _ = ⊤ᶜ + eval (# n) _ = [ + n ]ᶜ + + eval-Monoʳ : ∀ (e : Expr) → Monotonic _≼ᵛ_ _≼ᶜ_ (eval e) + eval-Monoʳ (e₁ + e₂) {vs₁} {vs₂} vs₁≼vs₂ = + eval-combine₂ (λ {x} {y} {z} → ≼ᶜ-trans {x} {y} {z}) + plus plus-Mono₂ {o₁ = eval e₁ vs₁} + (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ vs₁≼vs₂) + eval-Monoʳ (e₁ - e₂) {vs₁} {vs₂} vs₁≼vs₂ = + eval-combine₂ (λ {x} {y} {z} → ≼ᶜ-trans {x} {y} {z}) + minus minus-Mono₂ {o₁ = eval e₁ vs₁} + (eval-Monoʳ e₁ vs₁≼vs₂) (eval-Monoʳ e₂ 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 + (v₁ , k,v₁∈vs₁) = locateᵛ {k} {vs₁} k∈kvs₁ + (v₂ , k,v₂∈vs₂) = locateᵛ {k} {vs₂} k∈kvs₂ + in + m₁≼m₂⇒m₁[k]ᵛ≼m₂[k]ᵛ vs₁ vs₂ vs₁≼vs₂ k,v₁∈vs₁ k,v₂∈vs₂ + ... | 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ʳ (# n) _ = ≼ᶜ-refl ([ + n ]ᶜ) + + instance + ConstEval : ExprEvaluator + ConstEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ } + + -- For debugging purposes, print out the result. + output = show (Analysis.Forward.WithProg.result ConstLattice 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 + -- listing them all. + plus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ plus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.+ z₂)) + plus-valid {⊥ᶜ} {_} ⊥ _ = ⊥ + plus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥ + plus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥ + plus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt + plus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt + plus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl + plus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt + -- + -- Same for this one. It should be easier, but Agda won't simplify. + minus-valid : ∀ {g₁ g₂} {z₁ z₂} → ⟦ g₁ ⟧ᶜ (↑ᶻ z₁) → ⟦ g₂ ⟧ᶜ (↑ᶻ z₂) → ⟦ minus g₁ g₂ ⟧ᶜ (↑ᶻ (z₁ Int.- z₂)) + minus-valid {⊥ᶜ} {_} ⊥ _ = ⊥ + minus-valid {[ z ]ᶜ} {⊥ᶜ} _ ⊥ = ⊥ + minus-valid {⊤ᶜ} {⊥ᶜ} _ ⊥ = ⊥ + minus-valid {⊤ᶜ} {[ z ]ᶜ} _ _ = tt + minus-valid {⊤ᶜ} {⊤ᶜ} _ _ = tt + minus-valid {[ z₁ ]ᶜ} {[ z₂ ]ᶜ} refl refl = refl + minus-valid {[ z ]ᶜ} {⊤ᶜ} _ _ = tt + + 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⟧ρ = + 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 (⇒ᵉ-ℕ ρ n) _ = refl + + instance + ConstEvalValid : ValidExprEvaluator ConstEval latticeInterpretationᶜ + ConstEvalValid = record { valid = eval-valid } + + analyze-correct = Analysis.Forward.WithProg.analyze-correct ConstLattice prog tt diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index 9472414..ef0f67b 100644 --- a/Lattice/AboveBelow.agda +++ b/Lattice/AboveBelow.agda @@ -321,7 +321,7 @@ module Plain (x : A) where ; isLattice = isLattice } - open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public + open IsLattice isLattice using (_≼_; _≺_; ≼-trans; ≼-refl; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ] ⊥≺[x] x = (≈-refl , λ ()) diff --git a/Main.agda b/Main.agda index b7dbdb1..7686e74 100644 --- a/Main.agda +++ b/Main.agda @@ -1,11 +1,13 @@ {-# OPTIONS --guardedness #-} module Main where -open import Language -open import Analysis.Sign +open import Language hiding (_++_) open import Data.Vec using (Vec; _∷_; []) open import IO open import Level using (0ℓ) +open import Data.String using (_++_) +import Analysis.Constant as ConstantAnalysis +import Analysis.Sign as SignAnalysis testCode : Stmt testCode = @@ -38,6 +40,7 @@ testProgram = record { rootStmt = testCode } -open WithProg testProgram using (output; analyze-correct) +open SignAnalysis.WithProg testProgram using (analyze-correct) renaming (output to output-Sign) +open ConstantAnalysis.WithProg testProgram using (analyze-correct) renaming (output to output-Const) -main = run {0ℓ} (putStrLn output) +main = run {0ℓ} (putStrLn (output-Const ++ "\n" ++ output-Sign))