From ce062385a732d9f34577da3c144adbcb7659641c Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 16:20:36 +0800 Subject: [PATCH] =?UTF-8?q?Fix=20#288:=20[milestone=20Milestone=2012]=20`i?= =?UTF-8?q?nternal/symbolic/cache`=20=E2=80=94=20Decision=20cache=20for=20?= =?UTF-8?q?Z3=20queries:=20LRU=20cache=20keyed=20by=20...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- internal/symbolic/cache/cache.go | 164 ++++++++++++++++++++++++++ internal/symbolic/cache/cache_test.go | 77 ++++++++++++ internal/verify/z3.go | 18 ++- internal/z3/z3.go | 41 ++++++- 4 files changed, 297 insertions(+), 3 deletions(-) create mode 100644 internal/symbolic/cache/cache.go create mode 100644 internal/symbolic/cache/cache_test.go diff --git a/internal/symbolic/cache/cache.go b/internal/symbolic/cache/cache.go new file mode 100644 index 0000000..86128ad --- /dev/null +++ b/internal/symbolic/cache/cache.go @@ -0,0 +1,164 @@ +// Package cache provides a bounded LRU cache for completed Z3 decisions. +package cache + +import ( + "container/list" + "crypto/sha256" + "encoding/hex" + "os" + "strconv" + "sync" + "sync/atomic" +) + +const ( + // EnvMaxEntries configures the maximum number of Z3 decisions retained. + // A value of zero disables caching; invalid values use DefaultMaxEntries. + EnvMaxEntries = "SYMKERNEL_Z3_CACHE_SIZE" + + // DefaultMaxEntries bounds memory use when EnvMaxEntries is not set. + DefaultMaxEntries = 1_000 +) + +// Decision is a completed Z3 query result. Errors and timeout-driven unknown +// results are intentionally not cached by callers. +type Decision struct { + Sat string + Model map[string]any + UnsatCore []string +} + +// Stats is a snapshot of cache activity. +type Stats struct { + Entries int + MaxEntries int + Hits uint64 + Misses uint64 + Evictions uint64 +} + +type entry struct { + hash string + decision Decision +} + +// Cache is a concurrency-safe LRU cache keyed by an assertion hash. +type Cache struct { + mu sync.Mutex + maxEntries int + entries map[string]*list.Element + lru *list.List + hits uint64 + misses uint64 + evictions uint64 +} + +// New creates a decision cache with maxEntries entries. A negative size uses +// DefaultMaxEntries; zero disables caching. +func New(maxEntries int) *Cache { + if maxEntries < 0 { + maxEntries = DefaultMaxEntries + } + return &Cache{ + maxEntries: maxEntries, + entries: make(map[string]*list.Element), + lru: list.New(), + } +} + +// NewFromEnv creates a cache configured with SYMKERNEL_Z3_CACHE_SIZE. +func NewFromEnv() *Cache { + maxEntries := DefaultMaxEntries + if raw, ok := os.LookupEnv(EnvMaxEntries); ok { + if parsed, err := strconv.Atoi(raw); err == nil && parsed >= 0 { + maxEntries = parsed + } + } + return New(maxEntries) +} + +// HashAssertions returns the stable key for an SMT-LIB assertion program. +func HashAssertions(assertions string) string { + digest := sha256.Sum256([]byte(assertions)) + return hex.EncodeToString(digest[:]) +} + +// Get retrieves a completed decision and promotes it to most recently used. +func (c *Cache) Get(assertions string) (Decision, bool) { + return c.GetByHash(HashAssertions(assertions)) +} + +// GetByHash retrieves a completed decision by its precomputed assertion hash. +func (c *Cache) GetByHash(hash string) (Decision, bool) { + c.mu.Lock() + defer c.mu.Unlock() + + element, ok := c.entries[hash] + if !ok { + atomic.AddUint64(&c.misses, 1) + return Decision{}, false + } + c.lru.MoveToFront(element) + atomic.AddUint64(&c.hits, 1) + return cloneDecision(element.Value.(entry).decision), true +} + +// Set stores a completed decision, evicting the least recently used entry +// when the configured capacity is reached. +func (c *Cache) Set(assertions string, decision Decision) { + c.SetByHash(HashAssertions(assertions), decision) +} + +// SetByHash stores a completed decision under a precomputed assertion hash. +func (c *Cache) SetByHash(hash string, decision Decision) { + c.mu.Lock() + defer c.mu.Unlock() + + if c.maxEntries == 0 { + return + } + if element, ok := c.entries[hash]; ok { + element.Value = entry{hash: hash, decision: cloneDecision(decision)} + c.lru.MoveToFront(element) + return + } + + c.entries[hash] = c.lru.PushFront(entry{hash: hash, decision: cloneDecision(decision)}) + if c.lru.Len() <= c.maxEntries { + return + } + oldest := c.lru.Back() + oldEntry := oldest.Value.(entry) + delete(c.entries, oldEntry.hash) + c.lru.Remove(oldest) + atomic.AddUint64(&c.evictions, 1) +} + +// Stats returns a point-in-time cache snapshot. +func (c *Cache) Stats() Stats { + c.mu.Lock() + entries := len(c.entries) + maxEntries := c.maxEntries + c.mu.Unlock() + return Stats{ + Entries: entries, + MaxEntries: maxEntries, + Hits: atomic.LoadUint64(&c.hits), + Misses: atomic.LoadUint64(&c.misses), + Evictions: atomic.LoadUint64(&c.evictions), + } +} + +func cloneDecision(decision Decision) Decision { + copy := Decision{ + Sat: decision.Sat, + UnsatCore: append([]string(nil), decision.UnsatCore...), + } + if decision.Model != nil { + copy.Model = make(map[string]any, len(decision.Model)) + for key, value := range decision.Model { + copy.Model[key] = value + } + } + return copy +} diff --git a/internal/symbolic/cache/cache_test.go b/internal/symbolic/cache/cache_test.go new file mode 100644 index 0000000..e38d5c1 --- /dev/null +++ b/internal/symbolic/cache/cache_test.go @@ -0,0 +1,77 @@ +package cache + +import "testing" + +func TestCacheEvictsLeastRecentlyUsedDecision(t *testing.T) { + c := New(2) + c.Set("first", Decision{Sat: "sat"}) + c.Set("second", Decision{Sat: "unsat"}) + if _, ok := c.Get("first"); !ok { + t.Fatal("first decision was not cached") + } + c.Set("third", Decision{Sat: "unknown"}) + + if _, ok := c.Get("second"); ok { + t.Fatal("least recently used decision was retained") + } + if decision, ok := c.Get("first"); !ok || decision.Sat != "sat" { + t.Fatalf("first decision = %#v, %t; want cached sat decision", decision, ok) + } + if decision, ok := c.Get("third"); !ok || decision.Sat != "unknown" { + t.Fatalf("third decision = %#v, %t; want cached unknown decision", decision, ok) + } + + stats := c.Stats() + if stats.Evictions != 1 { + t.Errorf("evictions = %d, want 1", stats.Evictions) + } +} + +func TestCacheCopiesDecisionValues(t *testing.T) { + c := New(1) + c.Set("query", Decision{Sat: "sat", Model: map[string]any{"x": "1"}, UnsatCore: []string{"a"}}) + + decision, ok := c.Get("query") + if !ok { + t.Fatal("decision was not cached") + } + decision.Model["x"] = "changed" + decision.UnsatCore[0] = "changed" + + decision, ok = c.Get("query") + if !ok || decision.Model["x"] != "1" || decision.UnsatCore[0] != "a" { + t.Fatalf("cached decision was mutated: %#v, %t", decision, ok) + } +} + +func TestCacheUsesAssertionHash(t *testing.T) { + c := New(1) + assertions := "(assert (= x 1))" + c.Set(assertions, Decision{Sat: "sat"}) + + decision, ok := c.GetByHash(HashAssertions(assertions)) + if !ok || decision.Sat != "sat" { + t.Fatalf("decision = %#v, %t; want decision stored by assertion hash", decision, ok) + } +} + +func TestNewFromEnv(t *testing.T) { + t.Setenv(EnvMaxEntries, "2") + if got := NewFromEnv().Stats().MaxEntries; got != 2 { + t.Errorf("max entries = %d, want 2", got) + } + + t.Setenv(EnvMaxEntries, "invalid") + if got := NewFromEnv().Stats().MaxEntries; got != DefaultMaxEntries { + t.Errorf("invalid max entries = %d, want %d", got, DefaultMaxEntries) + } +} + +func TestNewFromEnvDisablesCacheAtZero(t *testing.T) { + t.Setenv(EnvMaxEntries, "0") + c := NewFromEnv() + c.Set("query", Decision{Sat: "sat"}) + if _, ok := c.Get("query"); ok { + t.Fatal("disabled cache returned a decision") + } +} diff --git a/internal/verify/z3.go b/internal/verify/z3.go index 21084f4..345bcde 100644 --- a/internal/verify/z3.go +++ b/internal/verify/z3.go @@ -5,6 +5,8 @@ import ( "fmt" "os/exec" "strings" + + "github.com/WasmAgent/symkernel/internal/symbolic/cache" ) // Result represents the outcome of an SMT2 constraint verification. @@ -25,9 +27,18 @@ type Solver interface { // Z3Solver invokes the z3 SMT solver as an external process. type Z3Solver struct{} +var z3DecisionCache = cache.NewFromEnv() + // Solve sends smt2 to the z3 binary via stdin (SMTLIB2 interactive mode) // and parses the check-sat result and optional model output. func (z *Z3Solver) Solve(ctx context.Context, smt2 string) (Result, error) { + if err := ctx.Err(); err != nil { + return Result{Sat: "unknown"}, nil + } + if decision, ok := z3DecisionCache.Get(smt2); ok { + return Result{Sat: decision.Sat, Model: decision.Model}, nil + } + cmd := exec.CommandContext(ctx, "z3", "-in") cmd.Stdin = strings.NewReader(smt2) @@ -44,16 +55,19 @@ func (z *Z3Solver) Solve(ctx context.Context, smt2 string) (Result, error) { return Result{}, fmt.Errorf("z3: empty output") } + var result Result switch lines[0] { case "sat": - return Result{Sat: "sat", Model: parseModel(lines[1:])}, nil + result = Result{Sat: "sat", Model: parseModel(lines[1:])} case "unsat": - return Result{Sat: "unsat", Model: nil}, nil + result = Result{Sat: "unsat", Model: nil} case "unknown": return Result{Sat: "unknown", Model: nil}, nil default: return Result{}, fmt.Errorf("z3: unexpected result %q", lines[0]) } + z3DecisionCache.Set(smt2, cache.Decision{Sat: result.Sat, Model: result.Model}) + return result, nil } // parseModel extracts variable bindings from z3 model output lines. diff --git a/internal/z3/z3.go b/internal/z3/z3.go index c909f24..941f0a1 100644 --- a/internal/z3/z3.go +++ b/internal/z3/z3.go @@ -9,8 +9,11 @@ import ( "context" "fmt" "os/exec" + "sort" "strings" "time" + + "github.com/WasmAgent/symkernel/internal/symbolic/cache" ) // Solution is the outcome of SolveConstraints. @@ -27,6 +30,8 @@ type Solution struct { SolverMs int64 `json:"solver_ms"` } +var decisionCache = cache.NewFromEnv() + // SolveConstraints submits an SMTLIB2 constraint string to Z3 and returns the // result. model is an optional map of variable name → sort hint (or concrete // Go value) used to emit (declare-const) declarations before the constraints. @@ -50,6 +55,12 @@ func SolveConstraints(constraints string, model map[string]any) (Solution, error // SolveConstraintsCtx is like SolveConstraints but honours the caller's ctx. func SolveConstraintsCtx(ctx context.Context, constraints string, model map[string]any) (Solution, error) { smt2 := buildSMT2(constraints, model) + if err := ctx.Err(); err != nil { + return Solution{Sat: "unknown"}, nil + } + if decision, ok := decisionCache.Get(smt2); ok { + return solutionFromDecision(decision), nil + } start := time.Now() cmd := exec.CommandContext(ctx, "z3", "-in") @@ -75,6 +86,9 @@ func SolveConstraintsCtx(ctx context.Context, constraints string, model map[stri sol, parseErr := parseOutput(stdout.String()) if parseErr == nil { sol.SolverMs = solverMs + if sol.Sat != "unknown" { + decisionCache.Set(smt2, decisionFromSolution(sol)) + } return sol, nil } } @@ -86,9 +100,28 @@ func SolveConstraintsCtx(ctx context.Context, constraints string, model map[stri return Solution{}, parseErr } sol.SolverMs = solverMs + if sol.Sat != "unknown" { + decisionCache.Set(smt2, decisionFromSolution(sol)) + } return sol, nil } +func decisionFromSolution(solution Solution) cache.Decision { + return cache.Decision{ + Sat: solution.Sat, + Model: solution.Model, + UnsatCore: solution.UnsatCore, + } +} + +func solutionFromDecision(decision cache.Decision) Solution { + return Solution{ + Sat: decision.Sat, + Model: decision.Model, + UnsatCore: decision.UnsatCore, + } +} + // hasNamedAssertions reports whether the constraints string uses SMTLIB2 // named assertions (:named keyword), which enables unsat-core extraction. func hasNamedAssertions(constraints string) bool { @@ -111,7 +144,13 @@ func buildSMT2(constraints string, model map[string]any) string { b.WriteString("(set-option :produce-unsat-cores true)\n") } - for name, val := range model { + names := make([]string, 0, len(model)) + for name := range model { + names = append(names, name) + } + sort.Strings(names) + for _, name := range names { + val := model[name] sort := inferSort(val) fmt.Fprintf(&b, "(declare-const %s %s)\n", name, sort) }