Fix #288: [milestone Milestone 12] internal/symbolic/cache — Decision cache for Z3 queries: LRU cache keyed by ...

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
+}

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")
+	}
+}

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.

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)
 	}