From f4961c2d90465a7a10baf5104aca42f2fcfb50d9 Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 20:16:15 +0800 Subject: [PATCH 01/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- cmd/symkerneld/routes_test.go | 17 +- internal/verify/symbolic.go | 721 ++++++++++++++++++++++++++++--- internal/verify/symbolic_test.go | 217 +++++----- 3 files changed, 767 insertions(+), 188 deletions(-) diff --git a/cmd/symkerneld/routes_test.go b/cmd/symkerneld/routes_test.go index 4f1e008..31a7ac3 100644 --- a/cmd/symkerneld/routes_test.go +++ b/cmd/symkerneld/routes_test.go @@ -55,21 +55,12 @@ func TestRegisterRoutes(t *testing.T) { t.Errorf("POST /v1/verify/z3 status = 404; route not mounted by RegisterRoutes") } - // The POST /v1/verify/symbolic placeholder route is mounted and responds - // 200 with its placeholder body, proving RegisterRoutes wired it. + // The POST /v1/verify/symbolic route is mounted: an empty request is + // rejected by its handler rather than falling through to the mux 404. sreq := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", nil) srec := httptest.NewRecorder() mux.ServeHTTP(srec, sreq) - if srec.Code != http.StatusOK { - t.Fatalf("POST /v1/verify/symbolic status = %d, want %d; route not mounted or wrong handler; body = %s", srec.Code, http.StatusOK, srec.Body.String()) - } - var sbody struct { - Message string `json:"message"` - } - if err := json.NewDecoder(srec.Body).Decode(&sbody); err != nil { - t.Fatalf("decode symbolic placeholder body: %v; body = %s", err, srec.Body.String()) - } - if sbody.Message != "Symbolic execution endpoint placeholder" { - t.Errorf("symbolic message = %q, want %q", sbody.Message, "Symbolic execution endpoint placeholder") + if srec.Code == http.StatusNotFound { + t.Errorf("POST /v1/verify/symbolic status = 404; route not mounted by RegisterRoutes") } } diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index 870932c..b399b70 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -1,93 +1,674 @@ -// Package verify provides the symbolic and SMT verification primitives used -// by symkerneld. The symbolic types in this file define the Milestone 3 -// contract that endpoint handlers wire against; Run is a stub until the -// full Z3-backed symbolic exploration engine lands. +// Package verify provides HTTP handlers for symkerneld verification endpoints. package verify import ( "context" + "encoding/base64" "encoding/json" - "errors" + "fmt" + "io" "net/http" + "strings" + "github.com/WasmAgent/symkernel/internal/z3" "github.com/google/uuid" ) -// ErrNotImplemented is returned by Run until the Z3-backed symbolic -// exploration engine is implemented. Endpoint handlers should still wire -// Run so the contract is exercised end-to-end while the engine matures. -var ErrNotImplemented = errors.New("symbolic verification not implemented") +const defaultSymbolicMaxDepth = 100 -// SymbolicInput is the request payload for symbolic verification: a base64 -// WebAssembly binary, the entry-point export to explore, and its arguments. +// SymbolicInput is the request payload for POST /v1/verify/symbolic. type SymbolicInput struct { - // WasmBinary is the base64-encoded WebAssembly module to explore. - WasmBinary string `json:"wasmBinary"` - // Entry names the export (function) to begin symbolic execution from. - Entry string `json:"entry"` - // Args are the initial argument values passed to Entry. - Args []any `json:"args"` + Module string `json:"module"` + Entrypoint string `json:"entrypoint"` + MaxDepth int `json:"maxDepth"` + PruneInfeasible bool `json:"pruneInfeasible"` } -// SymbolicPath describes one feasible execution path discovered during -// symbolic exploration: the guarding path constraint (SMT2) and a -// satisfying model. +// SymbolicPath is one terminal path reached by the entrypoint. type SymbolicPath struct { - // Constraints is the SMT2 path constraint that guards this path. - Constraints string `json:"constraints"` - // Model is a satisfying assignment for Constraints, keyed by symbol. - Model map[string]any `json:"model"` + ID string `json:"id"` + Feasible bool `json:"feasible"` + Constraints []string `json:"constraints"` + Output any `json:"output"` } -// SymbolicResult holds the set of explored paths and bookkeeping fields. +// SymbolicResult is the response payload for symbolic verification. type SymbolicResult struct { - // Paths is the set of feasible execution paths discovered. - Paths []SymbolicPath `json:"paths"` - // Explored is the total number of paths considered (feasible or not). - Explored int `json:"explored"` - // DecisionID is the per-call UUID, following the GENAI_SEMCONV field - // naming used across the WasmAgent ecosystem. Every response carries - // one for traceability — see CLAUDE.md "Bot instructions". - DecisionID string `json:"decision_id"` -} - -// Run executes symbolic exploration of in.WasmBinary starting at in.Entry. -// -// The engine is not yet implemented: Run always returns ErrNotImplemented -// alongside a result whose DecisionID is populated with a fresh UUID, so -// endpoint handlers can call it today and surface a decision_id to callers -// while the Z3-backed implementation lands. When ctx is cancelled the stub -// still returns the same sentinel rather than ctx.Err(), since no work is -// performed. + Paths []SymbolicPath `json:"paths"` + Explored int `json:"explored"` + Pruned int `json:"pruned"` + DecisionID string `json:"decision_id"` +} + +// Run symbolically executes the requested Wasm function. Function parameters +// become arg0, arg1, ... integer symbols. It deliberately supports the core +// integer/control-flow instruction set used for decisions; unsupported Wasm +// instructions fail explicitly instead of silently falling back to concrete +// execution. func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { - _ = ctx // no work performed by the stub; reserved for the real engine - _ = in - return SymbolicResult{DecisionID: uuid.NewString()}, ErrNotImplemented -} - -// symbolicPlaceholderResponse is the fixed acknowledgement body returned by -// SymbolicHandler while the symbolic execution engine is being built. -type symbolicPlaceholderResponse struct { - Message string `json:"message"` -} - -// SymbolicHandler returns an http.HandlerFunc for the POST /v1/verify/symbolic -// endpoint. -// -// It is a placeholder: the route contract, middleware wiring, and content -// type are exercised end-to-end, but no symbolic exploration is performed. -// It always responds 200 OK with -// {"message": "Symbolic execution endpoint placeholder"} so callers can detect -// that the route is mounted while the Z3-backed engine behind Run matures. It -// is a prerequisite for the full symbolic execution logic (issue #245): once -// Run is implemented, this handler will decode a SymbolicInput, call Run, and -// shape the SymbolicResult into the response. + if strings.TrimSpace(in.Module) == "" { + return SymbolicResult{}, fmt.Errorf("module is required") + } + if strings.TrimSpace(in.Entrypoint) == "" { + return SymbolicResult{}, fmt.Errorf("entrypoint is required") + } + if in.MaxDepth < 0 { + return SymbolicResult{}, fmt.Errorf("maxDepth must not be negative") + } + if in.MaxDepth == 0 { + in.MaxDepth = defaultSymbolicMaxDepth + } + wasm, err := base64.StdEncoding.DecodeString(in.Module) + if err != nil { + return SymbolicResult{}, fmt.Errorf("decode module: %w", err) + } + fn, err := parseExportedFunction(wasm, in.Entrypoint) + if err != nil { + return SymbolicResult{}, err + } + + initial := symbolicState{locals: make([]symbolicValue, len(fn.params)+len(fn.locals))} + model := make(map[string]any, len(fn.params)) + for i, typ := range fn.params { + if typ != valueI32 && typ != valueI64 { + return SymbolicResult{}, fmt.Errorf("entrypoint parameter %d has unsupported type 0x%x", i, typ) + } + name := fmt.Sprintf("arg%d", i) + initial.locals[i] = symbolicValue{expr: name} + model[name] = "Int" + } + + exec := executor{ctx: ctx, maxDepth: in.MaxDepth, prune: in.PruneInfeasible, model: model, explored: 1} + states, err := exec.run(fn.body, []symbolicState{initial}) + if err != nil { + return SymbolicResult{}, err + } + paths := make([]SymbolicPath, 0, len(states)) + for _, state := range states { + feasible, err := exec.feasible(state.constraints) + if err != nil { + return SymbolicResult{}, err + } + if !feasible && in.PruneInfeasible { + exec.pruned++ + continue + } + if len(state.stack) < len(fn.results) { + return SymbolicResult{}, fmt.Errorf("entrypoint %q did not produce its declared results", in.Entrypoint) + } + paths = append(paths, SymbolicPath{ + ID: uuid.NewString(), Feasible: feasible, Constraints: state.constraints, + Output: state.output(fn.results), + }) + } + return SymbolicResult{Paths: paths, Explored: exec.explored, Pruned: exec.pruned, DecisionID: uuid.NewString()}, nil +} + +type symbolicValue struct { + expr string + known *int64 +} + +func constant(v int64) symbolicValue { return symbolicValue{expr: fmt.Sprintf("%d", v), known: &v} } + +func (v symbolicValue) condition() string { + if v.known != nil { + if *v.known == 0 { + return "false" + } + return "true" + } + return "(not (= " + v.expr + " 0))" +} + +type symbolicState struct { + locals []symbolicValue + stack []symbolicValue + constraints []string + depth int +} + +func (s symbolicState) clone() symbolicState { + s.locals = append([]symbolicValue(nil), s.locals...) + s.stack = append([]symbolicValue(nil), s.stack...) + s.constraints = append([]string(nil), s.constraints...) + return s +} + +func (s *symbolicState) pop() (symbolicValue, error) { + if len(s.stack) == 0 { + return symbolicValue{}, fmt.Errorf("wasm stack underflow") + } + v := s.stack[len(s.stack)-1] + s.stack = s.stack[:len(s.stack)-1] + return v, nil +} + +func (s symbolicState) output(results []byte) any { + if len(results) == 0 { + return nil + } + values := make([]any, len(results)) + for i := range results { + v := s.stack[len(s.stack)-len(results)+i] + if v.known != nil { + if results[i] == valueI32 { + values[i] = int32(*v.known) + } else { + values[i] = *v.known + } + } else { + values[i] = v.expr + } + } + if len(values) == 1 { + return values[0] + } + return values +} + +type instruction struct { + opcode byte + index uint32 + value int64 + then []instruction + otherwise []instruction +} + +type executor struct { + ctx context.Context + maxDepth int + prune bool + model map[string]any + explored int + pruned int +} + +func (e *executor) run(program []instruction, states []symbolicState) ([]symbolicState, error) { + for _, in := range program { + next := make([]symbolicState, 0, len(states)) + for _, state := range states { + if err := e.ctx.Err(); err != nil { + return nil, err + } + state.depth++ + if state.depth > e.maxDepth { + e.pruned++ + continue + } + if in.opcode == 0x04 { // if + condition, err := state.pop() + if err != nil { + return nil, err + } + for _, branch := range []struct { + yes bool + code []instruction + }{{true, in.then}, {false, in.otherwise}} { + candidate := state.clone() + constraint := condition.condition() + if !branch.yes { + constraint = "(not " + constraint + ")" + } + candidate.constraints = append(candidate.constraints, constraint) + e.explored++ + if e.prune { + ok, err := e.feasible(candidate.constraints) + if err != nil { + return nil, err + } + if !ok { + e.pruned++ + continue + } + } + finished, err := e.run(branch.code, []symbolicState{candidate}) + if err != nil { + return nil, err + } + next = append(next, finished...) + } + continue + } + if err := executeInstruction(&state, in); err != nil { + return nil, err + } + next = append(next, state) + } + states = next + } + return states, nil +} + +func (e *executor) feasible(constraints []string) (bool, error) { + if len(constraints) == 0 { + return true, nil + } + var b strings.Builder + for _, c := range constraints { + fmt.Fprintf(&b, "(assert %s)\n", c) + } + solution, err := z3.SolveConstraintsCtx(e.ctx, b.String(), e.model) + if err != nil { + return false, fmt.Errorf("check path feasibility: %w", err) + } + return solution.Sat != "unsat", nil +} + +func executeInstruction(s *symbolicState, in instruction) error { + switch in.opcode { + case 0x20: // local.get + if int(in.index) >= len(s.locals) { + return fmt.Errorf("local index %d out of range", in.index) + } + s.stack = append(s.stack, s.locals[in.index]) + case 0x21, 0x22: // local.set / local.tee + v, err := s.pop() + if err != nil { + return err + } + if int(in.index) >= len(s.locals) { + return fmt.Errorf("local index %d out of range", in.index) + } + s.locals[in.index] = v + if in.opcode == 0x22 { + s.stack = append(s.stack, v) + } + case 0x41, 0x42: + s.stack = append(s.stack, constant(in.value)) // i32/i64.const + case 0x45: // i32.eqz + v, err := s.pop() + if err != nil { + return err + } + var known *bool + if v.known != nil { + value := *v.known == 0 + known = &value + } + s.stack = append(s.stack, boolValue("(= "+v.expr+" 0)", known)) + case 0x46, 0x47, 0x48, 0x4a, 0x4c, 0x4e: // eq, ne, lt_s, gt_s, le_s, ge_s + b, err := s.pop() + if err != nil { + return err + } + a, err := s.pop() + if err != nil { + return err + } + op := map[byte]string{0x46: "=", 0x47: "distinct", 0x48: "<", 0x4a: ">", 0x4c: "<=", 0x4e: ">="}[in.opcode] + var known *bool + if a.known != nil && b.known != nil { + value := compare(in.opcode, *a.known, *b.known) + known = &value + } + s.stack = append(s.stack, boolValue("("+op+" "+a.expr+" "+b.expr+")", known)) + case 0x6a, 0x6b, 0x6c: // i32.add/sub/mul + b, err := s.pop() + if err != nil { + return err + } + a, err := s.pop() + if err != nil { + return err + } + op := map[byte]string{0x6a: "+", 0x6b: "-", 0x6c: "*"}[in.opcode] + if a.known != nil && b.known != nil { + switch in.opcode { + case 0x6a: + s.stack = append(s.stack, constant(*a.known+*b.known)) + case 0x6b: + s.stack = append(s.stack, constant(*a.known-*b.known)) + default: + s.stack = append(s.stack, constant(*a.known**b.known)) + } + return nil + } + s.stack = append(s.stack, symbolicValue{expr: "(" + op + " " + a.expr + " " + b.expr + ")"}) + case 0x1a: + _, err := s.pop() + return err // drop + default: + return fmt.Errorf("unsupported symbolic wasm opcode 0x%x", in.opcode) + } + return nil +} + +func boolValue(expr string, value *bool) symbolicValue { + if value != nil { + if *value { + return constant(1) + } + return constant(0) + } + return symbolicValue{expr: expr} +} +func compare(op byte, a, b int64) bool { + switch op { + case 0x46: + return a == b + case 0x47: + return a != b + case 0x48: + return a < b + case 0x4a: + return a > b + case 0x4c: + return a <= b + default: + return a >= b + } +} + +const ( + valueI32 byte = 0x7f + valueI64 byte = 0x7e +) + +type wasmFunction struct { + params, results, locals []byte + body []instruction +} + +func parseExportedFunction(wasm []byte, entrypoint string) (wasmFunction, error) { + if len(wasm) < 8 || string(wasm[:4]) != "\x00asm" || string(wasm[4:8]) != "\x01\x00\x00\x00" { + return wasmFunction{}, fmt.Errorf("invalid wasm module") + } + types := [][]byte{} + functions := []uint32{} + codes := [][]byte{} + exports := map[string]uint32{} + imported := uint32(0) + p := 8 + for p < len(wasm) { + id := wasm[p] + p++ + n, next, err := readU32(wasm, p) + if err != nil { + return wasmFunction{}, err + } + p = next + if int(n) > len(wasm)-p { + return wasmFunction{}, fmt.Errorf("truncated wasm section") + } + section := wasm[p : p+int(n)] + p += int(n) + switch id { + case 1: + var err error + types, err = parseTypes(section) + if err != nil { + return wasmFunction{}, err + } + case 2: + count, _, err := readU32(section, 0) + if err != nil { + return wasmFunction{}, err + } + imported += count // imported functions are unsupported below + case 3: + functions, err = parseU32Vector(section) + if err != nil { + return wasmFunction{}, err + } + case 7: + exports, err = parseExports(section) + if err != nil { + return wasmFunction{}, err + } + case 10: + codes, err = parseCodes(section) + if err != nil { + return wasmFunction{}, err + } + } + } + idx, ok := exports[entrypoint] + if !ok { + return wasmFunction{}, fmt.Errorf("entrypoint %q is not an exported function", entrypoint) + } + if idx < imported || int(idx-imported) >= len(functions) || int(idx-imported) >= len(codes) { + return wasmFunction{}, fmt.Errorf("entrypoint %q uses an unsupported imported function", entrypoint) + } + typeIndex := functions[idx-imported] + if int(typeIndex) >= len(types) { + return wasmFunction{}, fmt.Errorf("invalid entrypoint type") + } + typeSig := types[typeIndex] + paramsCount := int(typeSig[0]) + resultsOffset := 1 + paramsCount + params := typeSig[1:resultsOffset] + results := typeSig[resultsOffset+1:] + locals, body, err := parseCode(codes[idx-imported]) + if err != nil { + return wasmFunction{}, err + } + return wasmFunction{params: params, results: results, locals: locals, body: body}, nil +} + +func parseTypes(b []byte) ([][]byte, error) { + count, p, err := readU32(b, 0) + if err != nil { + return nil, err + } + out := make([][]byte, 0, count) + for range count { + if p >= len(b) || b[p] != 0x60 { + return nil, fmt.Errorf("invalid wasm function type") + } + p++ + pc, n, err := readU32(b, p) + if err != nil { + return nil, err + } + p = n + if int(pc) > len(b)-p { + return nil, fmt.Errorf("truncated function params") + } + sig := []byte{byte(pc)} + sig = append(sig, b[p:p+int(pc)]...) + p += int(pc) + rc, n, err := readU32(b, p) + if err != nil { + return nil, err + } + p = n + if int(rc) > len(b)-p { + return nil, fmt.Errorf("truncated function results") + } + sig = append(sig, byte(rc)) + sig = append(sig, b[p:p+int(rc)]...) + p += int(rc) + out = append(out, sig) + } + return out, nil +} +func parseU32Vector(b []byte) ([]uint32, error) { + count, p, err := readU32(b, 0) + if err != nil { + return nil, err + } + out := make([]uint32, 0, count) + for range count { + v, n, err := readU32(b, p) + if err != nil { + return nil, err + } + p = n + out = append(out, v) + } + return out, nil +} +func parseExports(b []byte) (map[string]uint32, error) { + count, p, err := readU32(b, 0) + if err != nil { + return nil, err + } + out := map[string]uint32{} + for range count { + n, q, err := readU32(b, p) + if err != nil || int(n) > len(b)-q { + return nil, fmt.Errorf("invalid wasm export") + } + name := string(b[q : q+int(n)]) + p = q + int(n) + if p >= len(b) { + return nil, fmt.Errorf("truncated wasm export") + } + kind := b[p] + p++ + idx, q, err := readU32(b, p) + if err != nil { + return nil, err + } + p = q + if kind == 0 { + out[name] = idx + } + } + return out, nil +} +func parseCodes(b []byte) ([][]byte, error) { + count, p, err := readU32(b, 0) + if err != nil { + return nil, err + } + out := make([][]byte, 0, count) + for range count { + n, q, err := readU32(b, p) + if err != nil || int(n) > len(b)-q { + return nil, fmt.Errorf("invalid wasm code") + } + out = append(out, b[q:q+int(n)]) + p = q + int(n) + } + return out, nil +} +func parseCode(b []byte) ([]byte, []instruction, error) { + groups, p, err := readU32(b, 0) + if err != nil { + return nil, nil, err + } + var locals []byte + for range groups { + n, q, err := readU32(b, p) + if err != nil || q >= len(b) { + return nil, nil, fmt.Errorf("invalid wasm locals") + } + p = q + locals = append(locals, bytesRepeat(b[p], int(n))...) + p++ + } + body, p, stop, err := parseInstructions(b, p) + if err != nil { + return nil, nil, err + } + if stop != 0x0b || p != len(b) { + return nil, nil, fmt.Errorf("invalid wasm function body") + } + return locals, body, nil +} +func bytesRepeat(v byte, n int) []byte { + r := make([]byte, n) + for i := range r { + r[i] = v + } + return r +} +func parseInstructions(b []byte, p int) ([]instruction, int, byte, error) { + var out []instruction + for p < len(b) { + op := b[p] + p++ + if op == 0x0b || op == 0x05 { + return out, p, op, nil + } + in := instruction{opcode: op} + var err error + switch op { + case 0x04: + if p >= len(b) { + return nil, p, 0, fmt.Errorf("truncated if") + } + p++ + in.then, p, _, err = parseInstructions(b, p) + if err != nil { + return nil, p, 0, err + } + if p > 0 && b[p-1] == 0x05 { + in.otherwise, p, _, err = parseInstructions(b, p) + if err != nil { + return nil, p, 0, err + } + } + case 0x20, 0x21, 0x22: + in.index, p, err = readU32(b, p) + case 0x41, 0x42: + in.value, p, err = readS64(b, p) + } + if err != nil { + return nil, p, 0, err + } + out = append(out, in) + } + return nil, p, 0, fmt.Errorf("unterminated wasm instructions") +} +func readU32(b []byte, p int) (uint32, int, error) { + var v uint32 + for i := 0; i < 5; i++ { + if p >= len(b) { + return 0, p, fmt.Errorf("truncated wasm integer") + } + x := b[p] + p++ + v |= uint32(x&127) << uint(7*i) + if x&128 == 0 { + return v, p, nil + } + } + return 0, p, fmt.Errorf("invalid wasm integer") +} +func readS64(b []byte, p int) (int64, int, error) { + var v int64 + var shift uint + for { + if p >= len(b) || shift >= 64 { + return 0, p, fmt.Errorf("invalid wasm signed integer") + } + x := b[p] + p++ + v |= int64(x&127) << shift + shift += 7 + if x&128 == 0 { + if shift < 64 && x&64 != 0 { + v |= ^int64(0) << shift + } + return v, p, nil + } + } +} + +// SymbolicHandler returns the POST /v1/verify/symbolic endpoint handler. func SymbolicHandler() http.HandlerFunc { - return func(w http.ResponseWriter, _ *http.Request) { + return func(w http.ResponseWriter, r *http.Request) { + defer r.Body.Close() + var input SymbolicInput + decoder := json.NewDecoder(r.Body) + decoder.DisallowUnknownFields() + if err := decoder.Decode(&input); err != nil { + http.Error(w, fmt.Sprintf("invalid request: %v", err), http.StatusBadRequest) + return + } + if err := decoder.Decode(&struct{}{}); err != io.EOF { + http.Error(w, "invalid request: multiple JSON values", http.StatusBadRequest) + return + } + result, err := Run(r.Context(), input) + if err != nil { + http.Error(w, fmt.Sprintf("invalid symbolic execution request: %v", err), http.StatusBadRequest) + return + } w.Header().Set("Content-Type", "application/json") - w.WriteHeader(http.StatusOK) - _ = json.NewEncoder(w).Encode(symbolicPlaceholderResponse{ - Message: "Symbolic execution endpoint placeholder", - }) + _ = json.NewEncoder(w).Encode(result) } } diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index f518c34..7947903 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -2,8 +2,8 @@ package verify import ( "context" + "encoding/base64" "encoding/json" - "errors" "net/http" "net/http/httptest" "strings" @@ -12,146 +12,153 @@ import ( "github.com/google/uuid" ) -// TestRun_NotImplementedStub asserts the documented stub behaviour: Run -// returns ErrNotImplemented together with a result carrying a valid, -// freshly generated DecisionID, regardless of input. -func TestRun_NotImplementedStub(t *testing.T) { +func TestRun_ExecutesEntrypoint(t *testing.T) { t.Parallel() - tests := []struct { - name string - in SymbolicInput - }{ - { - name: "empty input", - in: SymbolicInput{}, - }, - { - name: "populated input", - in: SymbolicInput{ - WasmBinary: "AGVzbQ==", // arbitrary base64; not decoded by the stub - Entry: "_start", - Args: []any{1, "two", true}, - }, - }, - } - - for _, tt := range tests { - t.Run(tt.name, func(t *testing.T) { - t.Parallel() - - res, err := Run(context.Background(), tt.in) - - if !errors.Is(err, ErrNotImplemented) { - t.Fatalf("err = %v, want ErrNotImplemented", err) - } - - // The stub always returns a fresh decision UUID so handlers can - // surface a decision_id even before the engine is implemented. - if res.DecisionID == "" { - t.Fatal("DecisionID is empty, want a generated UUID") - } - if _, parseErr := uuid.Parse(res.DecisionID); parseErr != nil { - t.Errorf("DecisionID = %q is not a valid UUID: %v", res.DecisionID, parseErr) - } - - // No paths are explored by the stub. - if len(res.Paths) != 0 { - t.Errorf("Paths len = %d, want 0", len(res.Paths)) - } - if res.Explored != 0 { - t.Errorf("Explored = %d, want 0", res.Explored) - } - }) + result, err := Run(context.Background(), SymbolicInput{ + Module: wasmReturningI32(42), + Entrypoint: "main", + MaxDepth: 100, + }) + if err != nil { + t.Fatalf("Run() error = %v", err) + } + if result.Explored != 1 || result.Pruned != 0 { + t.Errorf("bookkeeping = explored:%d pruned:%d, want 1 and 0", result.Explored, result.Pruned) + } + if len(result.Paths) != 1 { + t.Fatalf("paths = %d, want 1", len(result.Paths)) + } + path := result.Paths[0] + if !path.Feasible || len(path.Constraints) != 0 || path.Output != int32(42) { + t.Errorf("path = %+v, want feasible empty-constraint path with output 42", path) + } + if _, err := uuid.Parse(path.ID); err != nil { + t.Errorf("path ID = %q is not a UUID: %v", path.ID, err) + } + if _, err := uuid.Parse(result.DecisionID); err != nil { + t.Errorf("decision ID = %q is not a UUID: %v", result.DecisionID, err) } } -// TestRun_ToleratesCancelledContext confirms the stub mints a decision_id -// even when the caller's context is already cancelled — no work is -// performed, so the sentinel is returned rather than ctx.Err(). -func TestRun_ToleratesCancelledContext(t *testing.T) { +func TestRun_RejectsInvalidInput(t *testing.T) { t.Parallel() - ctx, cancel := context.WithCancel(context.Background()) - cancel() - - res, err := Run(ctx, SymbolicInput{}) - if !errors.Is(err, ErrNotImplemented) { - t.Fatalf("err = %v, want ErrNotImplemented", err) - } - if res.DecisionID == "" { - t.Fatal("DecisionID is empty, want a generated UUID") + for _, input := range []SymbolicInput{ + {}, + {Module: "not base64", Entrypoint: "main"}, + {Module: wasmReturningI32(1), Entrypoint: "missing"}, + {Module: wasmReturningI32(1), Entrypoint: "main", MaxDepth: -1}, + } { + if _, err := Run(context.Background(), input); err == nil { + t.Errorf("Run(%+v) error = nil, want validation error", input) + } } } -// TestRun_DecisionIDIsUnique confirms each call mints a distinct decision_id. -func TestRun_DecisionIDIsUnique(t *testing.T) { +func TestRun_ExploresBranchesAndHonorsControls(t *testing.T) { t.Parallel() - a, errA := Run(context.Background(), SymbolicInput{}) - b, errB := Run(context.Background(), SymbolicInput{}) + input := SymbolicInput{Module: wasmNestedBranch(), Entrypoint: "main", MaxDepth: 100} + withoutPruning, err := Run(context.Background(), input) + if err != nil { + t.Fatalf("Run() without pruning error = %v", err) + } + if withoutPruning.Explored != 5 || withoutPruning.Pruned != 0 || len(withoutPruning.Paths) != 3 { + t.Fatalf("without pruning = %+v, want five explored and three returned paths", withoutPruning) + } + var infeasible int + for _, path := range withoutPruning.Paths { + if !path.Feasible { + infeasible++ + } + } + if infeasible != 1 { + t.Errorf("infeasible paths = %d, want 1", infeasible) + } - if !errors.Is(errA, ErrNotImplemented) || !errors.Is(errB, ErrNotImplemented) { - t.Fatalf("errors = %v, %v; both want ErrNotImplemented", errA, errB) + input.PruneInfeasible = true + pruned, err := Run(context.Background(), input) + if err != nil { + t.Fatalf("Run() with pruning error = %v", err) } - if a.DecisionID == "" { - t.Fatal("first DecisionID is empty") + if pruned.Explored != 5 || pruned.Pruned != 1 || len(pruned.Paths) != 2 { + t.Errorf("with pruning = %+v, want 5 explored, 1 pruned, 2 paths", pruned) } - if a.DecisionID == b.DecisionID { - t.Fatalf("DecisionIDs collided: %s", a.DecisionID) + + input.MaxDepth = 1 + depthLimited, err := Run(context.Background(), input) + if err != nil { + t.Fatalf("Run() with depth limit error = %v", err) + } + if len(depthLimited.Paths) != 0 || depthLimited.Pruned == 0 { + t.Errorf("depth-limited result = %+v, want no completed paths and pruned work", depthLimited) } } -// TestSymbolicHandler_Placeholder asserts the documented placeholder -// behaviour: SymbolicHandler always responds 200 OK with the fixed -// acknowledgement body and a JSON content type, regardless of the request -// body, so the /v1/verify/symbolic route contract is exercised end-to-end -// while the symbolic engine matures. -func TestSymbolicHandler_Placeholder(t *testing.T) { +func TestSymbolicHandler(t *testing.T) { t.Parallel() - handler := SymbolicHandler() - - // The handler is a placeholder that ignores the body; send a plausible - // symbolic request to prove no parsing is attempted yet. - body := `{"input":{"wasmBinary":"AGVzbQ==","entry":"_start","args":[]}}` + body := `{"module":"` + wasmReturningI32(7) + `","entrypoint":"main","maxDepth":100,"pruneInfeasible":true}` req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", strings.NewReader(body)) - req.Header.Set("Content-Type", "application/json") rec := httptest.NewRecorder() - handler.ServeHTTP(rec, req) + SymbolicHandler().ServeHTTP(rec, req) if rec.Code != http.StatusOK { t.Fatalf("status = %d, want %d; body = %s", rec.Code, http.StatusOK, rec.Body.String()) } - if ct := rec.Header().Get("Content-Type"); ct != "application/json" { - t.Errorf("Content-Type = %q, want %q", ct, "application/json") + if contentType := rec.Header().Get("Content-Type"); contentType != "application/json" { + t.Errorf("Content-Type = %q, want application/json", contentType) } - - var resp symbolicPlaceholderResponse - if err := json.NewDecoder(rec.Body).Decode(&resp); err != nil { - t.Fatalf("decode response: %v; body = %s", err, rec.Body.String()) + var result SymbolicResult + if err := json.NewDecoder(rec.Body).Decode(&result); err != nil { + t.Fatalf("decode response: %v", err) } - const want = "Symbolic execution endpoint placeholder" - if resp.Message != want { - t.Errorf("message = %q, want %q", resp.Message, want) + if len(result.Paths) != 1 || result.Paths[0].Output != float64(7) { + t.Errorf("response = %+v, want one path with output 7", result) } } -// TestSymbolicHandler_IgnoresEmptyBody confirms the placeholder responds 200 -// even when no body is posted, matching how the route is exercised through the -// registered mux (e.g. liveness-style probes). -func TestSymbolicHandler_IgnoresEmptyBody(t *testing.T) { +func TestSymbolicHandler_RejectsInvalidRequest(t *testing.T) { t.Parallel() - handler := SymbolicHandler() + for _, body := range []string{ + `{"module":"not-base64","entrypoint":"main"}`, + `{"module":"` + wasmReturningI32(1) + `","entrypoint":"main"} {}`, + } { + req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", strings.NewReader(body)) + rec := httptest.NewRecorder() - req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", nil) - rec := httptest.NewRecorder() + SymbolicHandler().ServeHTTP(rec, req) - handler.ServeHTTP(rec, req) + if rec.Code != http.StatusBadRequest { + t.Errorf("status = %d, want %d; body = %s", rec.Code, http.StatusBadRequest, rec.Body.String()) + } + } +} - if rec.Code != http.StatusOK { - t.Fatalf("status = %d, want %d; body = %s", rec.Code, http.StatusOK, rec.Body.String()) +func wasmReturningI32(value byte) string { + wasm := []byte{ + 0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, + 0x01, 0x05, 0x01, 0x60, 0x00, 0x01, 0x7f, + 0x03, 0x02, 0x01, 0x00, + 0x07, 0x08, 0x01, 0x04, 0x6d, 0x61, 0x69, 0x6e, 0x00, 0x00, + 0x0a, 0x06, 0x01, 0x04, 0x00, 0x41, value, 0x0b, + } + return base64.StdEncoding.EncodeToString(wasm) +} + +func wasmNestedBranch() string { + wasm := []byte{ + 0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, + 0x01, 0x06, 0x01, 0x60, 0x01, 0x7f, 0x01, 0x7f, + 0x03, 0x02, 0x01, 0x00, + 0x07, 0x08, 0x01, 0x04, 0x6d, 0x61, 0x69, 0x6e, 0x00, 0x00, + 0x0a, 0x16, 0x01, 0x14, 0x00, + 0x20, 0x00, 0x04, 0x7f, + 0x20, 0x00, 0x04, 0x7f, 0x41, 0x01, 0x05, 0x41, 0x02, 0x0b, + 0x05, 0x41, 0x03, 0x0b, 0x0b, } + return base64.StdEncoding.EncodeToString(wasm) } From c709a7fca79cb1e148868564d9cd444dbad29f7e Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 20:53:07 +0800 Subject: [PATCH 02/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- cmd/symkerneld/routes_test.go | 4 +- internal/verify/symbolic.go | 108 ++++++++++++++++++++++++++----- internal/verify/symbolic_test.go | 104 +++++++++++++++++++++++++++++ 3 files changed, 198 insertions(+), 18 deletions(-) diff --git a/cmd/symkerneld/routes_test.go b/cmd/symkerneld/routes_test.go index 31a7ac3..dbe2bcc 100644 --- a/cmd/symkerneld/routes_test.go +++ b/cmd/symkerneld/routes_test.go @@ -60,7 +60,7 @@ func TestRegisterRoutes(t *testing.T) { sreq := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", nil) srec := httptest.NewRecorder() mux.ServeHTTP(srec, sreq) - if srec.Code == http.StatusNotFound { - t.Errorf("POST /v1/verify/symbolic status = 404; route not mounted by RegisterRoutes") + if srec.Code != http.StatusBadRequest { + t.Errorf("POST /v1/verify/symbolic status = %d, want %d; body = %s", srec.Code, http.StatusBadRequest, srec.Body.String()) } } diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index b399b70..3e8c85d 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -14,7 +14,19 @@ import ( "github.com/google/uuid" ) -const defaultSymbolicMaxDepth = 100 +const ( + defaultSymbolicMaxDepth = 100 + maxSymbolicMaxDepth = 256 + maxSymbolicExplored = 4096 + maxSymbolicRequestBytes = 2 << 20 + maxSymbolicModuleBytes = 1 << 20 + maxSymbolicEntrypointLen = 256 + maxWasmVectorItems = 4096 + maxWasmParams = 64 + maxWasmLocals = 4096 + maxWasmInstructions = 16384 + maxWasmControlDepth = 256 +) // SymbolicInput is the request payload for POST /v1/verify/symbolic. type SymbolicInput struct { @@ -52,16 +64,29 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { if strings.TrimSpace(in.Entrypoint) == "" { return SymbolicResult{}, fmt.Errorf("entrypoint is required") } + if len(in.Entrypoint) > maxSymbolicEntrypointLen { + return SymbolicResult{}, fmt.Errorf("entrypoint exceeds %d bytes", maxSymbolicEntrypointLen) + } if in.MaxDepth < 0 { return SymbolicResult{}, fmt.Errorf("maxDepth must not be negative") } if in.MaxDepth == 0 { in.MaxDepth = defaultSymbolicMaxDepth } + if in.MaxDepth > maxSymbolicMaxDepth { + return SymbolicResult{}, fmt.Errorf("maxDepth must not exceed %d", maxSymbolicMaxDepth) + } + maxEncodedModule := 4 * ((maxSymbolicModuleBytes + 2) / 3) + if len(in.Module) > maxEncodedModule { + return SymbolicResult{}, fmt.Errorf("module exceeds %d decoded bytes", maxSymbolicModuleBytes) + } wasm, err := base64.StdEncoding.DecodeString(in.Module) if err != nil { return SymbolicResult{}, fmt.Errorf("decode module: %w", err) } + if len(wasm) > maxSymbolicModuleBytes { + return SymbolicResult{}, fmt.Errorf("module exceeds %d bytes", maxSymbolicModuleBytes) + } fn, err := parseExportedFunction(wasm, in.Entrypoint) if err != nil { return SymbolicResult{}, err @@ -105,13 +130,23 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { } type symbolicValue struct { - expr string - known *int64 + expr string + known *int64 + boolean bool } func constant(v int64) symbolicValue { return symbolicValue{expr: fmt.Sprintf("%d", v), known: &v} } func (v symbolicValue) condition() string { + if v.boolean { + if v.known != nil { + if *v.known == 0 { + return "false" + } + return "true" + } + return v.expr + } if v.known != nil { if *v.known == 0 { return "false" @@ -211,6 +246,9 @@ func (e *executor) run(program []instruction, states []symbolicState) ([]symboli constraint = "(not " + constraint + ")" } candidate.constraints = append(candidate.constraints, constraint) + if e.explored >= maxSymbolicExplored { + return nil, fmt.Errorf("symbolic execution exceeded the %d path limit", maxSymbolicExplored) + } e.explored++ if e.prune { ok, err := e.feasible(candidate.constraints) @@ -252,7 +290,14 @@ func (e *executor) feasible(constraints []string) (bool, error) { if err != nil { return false, fmt.Errorf("check path feasibility: %w", err) } - return solution.Sat != "unsat", nil + switch solution.Sat { + case "sat": + return true, nil + case "unsat": + return false, nil + default: + return false, fmt.Errorf("check path feasibility: z3 returned %q", solution.Sat) + } } func executeInstruction(s *symbolicState, in instruction) error { @@ -336,12 +381,13 @@ func executeInstruction(s *symbolicState, in instruction) error { func boolValue(expr string, value *bool) symbolicValue { if value != nil { + known := int64(0) if *value { - return constant(1) + known = 1 } - return constant(0) + return symbolicValue{expr: fmt.Sprintf("%t", *value), known: &known, boolean: true} } - return symbolicValue{expr: expr} + return symbolicValue{expr: expr, boolean: true} } func compare(op byte, a, b int64) bool { switch op { @@ -405,6 +451,9 @@ func parseExportedFunction(wasm []byte, entrypoint string) (wasmFunction, error) if err != nil { return wasmFunction{}, err } + if count > maxWasmVectorItems || imported > maxWasmVectorItems-count { + return wasmFunction{}, fmt.Errorf("too many wasm imports") + } imported += count // imported functions are unsupported below case 3: functions, err = parseU32Vector(section) @@ -451,7 +500,10 @@ func parseTypes(b []byte) ([][]byte, error) { if err != nil { return nil, err } - out := make([][]byte, 0, count) + if count > maxWasmVectorItems || int(count) > len(b) { + return nil, fmt.Errorf("too many wasm types") + } + out := make([][]byte, 0, int(count)) for range count { if p >= len(b) || b[p] != 0x60 { return nil, fmt.Errorf("invalid wasm function type") @@ -462,7 +514,7 @@ func parseTypes(b []byte) ([][]byte, error) { return nil, err } p = n - if int(pc) > len(b)-p { + if pc > maxWasmParams || int(pc) > len(b)-p { return nil, fmt.Errorf("truncated function params") } sig := []byte{byte(pc)} @@ -473,7 +525,7 @@ func parseTypes(b []byte) ([][]byte, error) { return nil, err } p = n - if int(rc) > len(b)-p { + if rc > maxWasmParams || int(rc) > len(b)-p { return nil, fmt.Errorf("truncated function results") } sig = append(sig, byte(rc)) @@ -488,7 +540,10 @@ func parseU32Vector(b []byte) ([]uint32, error) { if err != nil { return nil, err } - out := make([]uint32, 0, count) + if count > maxWasmVectorItems || int(count) > len(b)-p { + return nil, fmt.Errorf("too many wasm vector items") + } + out := make([]uint32, 0, int(count)) for range count { v, n, err := readU32(b, p) if err != nil { @@ -504,7 +559,10 @@ func parseExports(b []byte) (map[string]uint32, error) { if err != nil { return nil, err } - out := map[string]uint32{} + if count > maxWasmVectorItems || int(count) > len(b)-p { + return nil, fmt.Errorf("too many wasm exports") + } + out := make(map[string]uint32, int(count)) for range count { n, q, err := readU32(b, p) if err != nil || int(n) > len(b)-q { @@ -533,7 +591,10 @@ func parseCodes(b []byte) ([][]byte, error) { if err != nil { return nil, err } - out := make([][]byte, 0, count) + if count > maxWasmVectorItems || int(count) > len(b)-p { + return nil, fmt.Errorf("too many wasm code bodies") + } + out := make([][]byte, 0, int(count)) for range count { n, q, err := readU32(b, p) if err != nil || int(n) > len(b)-q { @@ -549,10 +610,13 @@ func parseCode(b []byte) ([]byte, []instruction, error) { if err != nil { return nil, nil, err } + if groups > maxWasmVectorItems || int(groups) > len(b)-p { + return nil, nil, fmt.Errorf("too many wasm local groups") + } var locals []byte for range groups { n, q, err := readU32(b, p) - if err != nil || q >= len(b) { + if err != nil || q >= len(b) || n > maxWasmLocals || uint64(len(locals))+uint64(n) > maxWasmLocals { return nil, nil, fmt.Errorf("invalid wasm locals") } p = q @@ -576,6 +640,10 @@ func bytesRepeat(v byte, n int) []byte { return r } func parseInstructions(b []byte, p int) ([]instruction, int, byte, error) { + return parseInstructionsWithBudget(b, p, new(int), 0) +} + +func parseInstructionsWithBudget(b []byte, p int, instructionCount *int, controlDepth int) ([]instruction, int, byte, error) { var out []instruction for p < len(b) { op := b[p] @@ -584,19 +652,26 @@ func parseInstructions(b []byte, p int) ([]instruction, int, byte, error) { return out, p, op, nil } in := instruction{opcode: op} + (*instructionCount)++ + if *instructionCount > maxWasmInstructions { + return nil, p, 0, fmt.Errorf("too many wasm instructions") + } var err error switch op { case 0x04: + if controlDepth >= maxWasmControlDepth { + return nil, p, 0, fmt.Errorf("wasm control nesting exceeds %d", maxWasmControlDepth) + } if p >= len(b) { return nil, p, 0, fmt.Errorf("truncated if") } p++ - in.then, p, _, err = parseInstructions(b, p) + in.then, p, _, err = parseInstructionsWithBudget(b, p, instructionCount, controlDepth+1) if err != nil { return nil, p, 0, err } if p > 0 && b[p-1] == 0x05 { - in.otherwise, p, _, err = parseInstructions(b, p) + in.otherwise, p, _, err = parseInstructionsWithBudget(b, p, instructionCount, controlDepth+1) if err != nil { return nil, p, 0, err } @@ -652,6 +727,7 @@ func readS64(b []byte, p int) (int64, int, error) { func SymbolicHandler() http.HandlerFunc { return func(w http.ResponseWriter, r *http.Request) { defer r.Body.Close() + r.Body = http.MaxBytesReader(w, r.Body, maxSymbolicRequestBytes) var input SymbolicInput decoder := json.NewDecoder(r.Body) decoder.DisallowUnknownFields() diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index 7947903..ed571d3 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -49,6 +49,7 @@ func TestRun_RejectsInvalidInput(t *testing.T) { {Module: "not base64", Entrypoint: "main"}, {Module: wasmReturningI32(1), Entrypoint: "missing"}, {Module: wasmReturningI32(1), Entrypoint: "main", MaxDepth: -1}, + {Module: wasmReturningI32(1), Entrypoint: "main", MaxDepth: maxSymbolicMaxDepth + 1}, } { if _, err := Run(context.Background(), input); err == nil { t.Errorf("Run(%+v) error = nil, want validation error", input) @@ -56,6 +57,41 @@ func TestRun_RejectsInvalidInput(t *testing.T) { } } +func TestSymbolicComparisonConditionPreservesBoolExpression(t *testing.T) { + t.Parallel() + + state := symbolicState{locals: []symbolicValue{{expr: "arg0"}}} + for _, instruction := range []instruction{ + {opcode: 0x20, index: 0}, + {opcode: 0x41, value: 0}, + {opcode: 0x46}, + } { + if err := executeInstruction(&state, instruction); err != nil { + t.Fatalf("executeInstruction(%#x) error = %v", instruction.opcode, err) + } + } + condition, err := state.pop() + if err != nil { + t.Fatalf("pop() error = %v", err) + } + if got, want := condition.condition(), "(= arg0 0)"; got != want { + t.Errorf("condition() = %q, want %q", got, want) + } +} + +func TestRun_EnforcesGlobalPathLimit(t *testing.T) { + t.Parallel() + + _, err := Run(context.Background(), SymbolicInput{ + Module: wasmSequentialBranches(12), + Entrypoint: "main", + MaxDepth: maxSymbolicMaxDepth, + }) + if err == nil || !strings.Contains(err.Error(), "path limit") { + t.Fatalf("Run() error = %v, want global path limit error", err) + } +} + func TestRun_ExploresBranchesAndHonorsControls(t *testing.T) { t.Parallel() @@ -138,6 +174,37 @@ func TestSymbolicHandler_RejectsInvalidRequest(t *testing.T) { } } +func TestSymbolicHandler_RejectsOversizedRequest(t *testing.T) { + t.Parallel() + + req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", strings.NewReader(strings.Repeat("x", maxSymbolicRequestBytes+1))) + rec := httptest.NewRecorder() + + SymbolicHandler().ServeHTTP(rec, req) + + if rec.Code != http.StatusBadRequest { + t.Fatalf("status = %d, want %d", rec.Code, http.StatusBadRequest) + } +} + +func TestWasmParserRejectsOversizedVectors(t *testing.T) { + t.Parallel() + + tooMany := []byte{0xff, 0xff, 0xff, 0xff, 0x0f} + if _, err := parseTypes(tooMany); err == nil { + t.Error("parseTypes() error = nil, want vector limit error") + } + if _, err := parseU32Vector(tooMany); err == nil { + t.Error("parseU32Vector() error = nil, want vector limit error") + } + if _, err := parseExports(tooMany); err == nil { + t.Error("parseExports() error = nil, want vector limit error") + } + if _, err := parseCodes(tooMany); err == nil { + t.Error("parseCodes() error = nil, want vector limit error") + } +} + func wasmReturningI32(value byte) string { wasm := []byte{ 0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, @@ -162,3 +229,40 @@ func wasmNestedBranch() string { } return base64.StdEncoding.EncodeToString(wasm) } + +func wasmSequentialBranches(count int) string { + body := []byte{0x00} // no locals + for range count { + body = append(body, 0x20, 0x00, 0x04, 0x7f, 0x41, 0x01, 0x05, 0x41, 0x02, 0x0b) + } + body = append(body, 0x0b) + + code := append([]byte{0x01}, wasmU32(uint32(len(body)))...) + code = append(code, body...) + wasm := []byte{0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00} + wasm = append(wasm, wasmSection(1, []byte{0x01, 0x60, 0x01, 0x7f, 0x01, 0x7f})...) + wasm = append(wasm, wasmSection(3, []byte{0x01, 0x00})...) + wasm = append(wasm, wasmSection(7, []byte{0x01, 0x04, 'm', 'a', 'i', 'n', 0x00, 0x00})...) + wasm = append(wasm, wasmSection(10, code)...) + return base64.StdEncoding.EncodeToString(wasm) +} + +func wasmSection(id byte, payload []byte) []byte { + section := append([]byte{id}, wasmU32(uint32(len(payload)))...) + return append(section, payload...) +} + +func wasmU32(value uint32) []byte { + var out []byte + for { + b := byte(value & 0x7f) + value >>= 7 + if value != 0 { + b |= 0x80 + } + out = append(out, b) + if value == 0 { + return out + } + } +} From 7ffd55198e368f5766dd35539e4e46b3707399b0 Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 21:16:23 +0800 Subject: [PATCH 03/10] Fix #287: implement symbolic WASM verification endpoint --- internal/verify/symbolic.go | 262 +++++++++++++++++++++++++------ internal/verify/symbolic_test.go | 65 +++++++- 2 files changed, 277 insertions(+), 50 deletions(-) diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index 3e8c85d..0b4186b 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -2,6 +2,7 @@ package verify import ( + "bytes" "context" "encoding/base64" "encoding/json" @@ -34,6 +35,12 @@ type SymbolicInput struct { Entrypoint string `json:"entrypoint"` MaxDepth int `json:"maxDepth"` PruneInfeasible bool `json:"pruneInfeasible"` + + // WasmBinary, Entry, and Args are retained for callers of the original + // symbolic API. Module and Entrypoint are the endpoint field names. + WasmBinary string `json:"wasmBinary,omitempty"` + Entry string `json:"entry,omitempty"` + Args []any `json:"args,omitempty"` } // SymbolicPath is one terminal path reached by the entrypoint. @@ -52,21 +59,39 @@ type SymbolicResult struct { DecisionID string `json:"decision_id"` } -// Run symbolically executes the requested Wasm function. Function parameters -// become arg0, arg1, ... integer symbols. It deliberately supports the core -// integer/control-flow instruction set used for decisions; unsupported Wasm -// instructions fail explicitly instead of silently falling back to concrete -// execution. +// Run symbolically executes the requested Wasm function. Unbound function +// parameters become fixed-width arg0, arg1, ... bitvector symbols. It +// deliberately supports the core integer/control-flow instruction set used +// for decisions; unsupported Wasm instructions fail explicitly instead of +// silently falling back to concrete execution. func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { - if strings.TrimSpace(in.Module) == "" { + module := strings.TrimSpace(in.Module) + if module == "" { + module = strings.TrimSpace(in.WasmBinary) + } else if legacy := strings.TrimSpace(in.WasmBinary); legacy != "" && legacy != module { + return SymbolicResult{}, fmt.Errorf("module and wasmBinary disagree") + } + if module == "" { return SymbolicResult{}, fmt.Errorf("module is required") } - if strings.TrimSpace(in.Entrypoint) == "" { + entrypoint := strings.TrimSpace(in.Entrypoint) + if entrypoint == "" { + entrypoint = strings.TrimSpace(in.Entry) + } else if legacy := strings.TrimSpace(in.Entry); legacy != "" && legacy != entrypoint { + return SymbolicResult{}, fmt.Errorf("entrypoint and entry disagree") + } + if entrypoint == "" { return SymbolicResult{}, fmt.Errorf("entrypoint is required") } - if len(in.Entrypoint) > maxSymbolicEntrypointLen { + if len(entrypoint) > maxSymbolicEntrypointLen { return SymbolicResult{}, fmt.Errorf("entrypoint exceeds %d bytes", maxSymbolicEntrypointLen) } + if ctx == nil { + ctx = context.Background() + } + if err := ctx.Err(); err != nil { + return SymbolicResult{}, err + } if in.MaxDepth < 0 { return SymbolicResult{}, fmt.Errorf("maxDepth must not be negative") } @@ -77,17 +102,17 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { return SymbolicResult{}, fmt.Errorf("maxDepth must not exceed %d", maxSymbolicMaxDepth) } maxEncodedModule := 4 * ((maxSymbolicModuleBytes + 2) / 3) - if len(in.Module) > maxEncodedModule { + if len(module) > maxEncodedModule { return SymbolicResult{}, fmt.Errorf("module exceeds %d decoded bytes", maxSymbolicModuleBytes) } - wasm, err := base64.StdEncoding.DecodeString(in.Module) + wasm, err := base64.StdEncoding.DecodeString(module) if err != nil { return SymbolicResult{}, fmt.Errorf("decode module: %w", err) } if len(wasm) > maxSymbolicModuleBytes { return SymbolicResult{}, fmt.Errorf("module exceeds %d bytes", maxSymbolicModuleBytes) } - fn, err := parseExportedFunction(wasm, in.Entrypoint) + fn, err := parseExportedFunction(wasm, entrypoint) if err != nil { return SymbolicResult{}, err } @@ -95,12 +120,28 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { initial := symbolicState{locals: make([]symbolicValue, len(fn.params)+len(fn.locals))} model := make(map[string]any, len(fn.params)) for i, typ := range fn.params { - if typ != valueI32 && typ != valueI64 { + bits, ok := wasmIntegerWidth(typ) + if !ok { return SymbolicResult{}, fmt.Errorf("entrypoint parameter %d has unsupported type 0x%x", i, typ) } + if i < len(in.Args) && in.Args[i] != nil { + value, err := concreteArgument(in.Args[i], bits) + if err != nil { + return SymbolicResult{}, fmt.Errorf("argument %d: %w", i, err) + } + initial.locals[i] = value + continue + } name := fmt.Sprintf("arg%d", i) - initial.locals[i] = symbolicValue{expr: name} - model[name] = "Int" + initial.locals[i] = symbolicValue{expr: name, bits: bits} + model[name] = fmt.Sprintf("BitVec_%d", bits) + } + for i, typ := range fn.locals { + bits, ok := wasmIntegerWidth(typ) + if !ok { + return SymbolicResult{}, fmt.Errorf("entrypoint local %d has unsupported type 0x%x", i, typ) + } + initial.locals[len(fn.params)+i] = typedConstant(0, bits) } exec := executor{ctx: ctx, maxDepth: in.MaxDepth, prune: in.PruneInfeasible, model: model, explored: 1} @@ -119,7 +160,7 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { continue } if len(state.stack) < len(fn.results) { - return SymbolicResult{}, fmt.Errorf("entrypoint %q did not produce its declared results", in.Entrypoint) + return SymbolicResult{}, fmt.Errorf("entrypoint %q did not produce its declared results", entrypoint) } paths = append(paths, SymbolicPath{ ID: uuid.NewString(), Feasible: feasible, Constraints: state.constraints, @@ -133,9 +174,74 @@ type symbolicValue struct { expr string known *int64 boolean bool + bits byte } -func constant(v int64) symbolicValue { return symbolicValue{expr: fmt.Sprintf("%d", v), known: &v} } +func typedConstant(v int64, bits byte) symbolicValue { + v = wrapSigned(v, bits) + unsigned := uint64(v) + if bits < 64 { + unsigned &= (uint64(1) << bits) - 1 + } + return symbolicValue{expr: fmt.Sprintf("(_ bv%d %d)", unsigned, bits), known: &v, bits: bits} +} + +func wrapSigned(v int64, bits byte) int64 { + if bits == 32 { + return int64(int32(v)) + } + return v +} + +func (v symbolicValue) zeroExpr() string { + return fmt.Sprintf("(_ bv0 %d)", v.bits) +} + +func concreteArgument(value any, bits byte) (symbolicValue, error) { + var number int64 + switch v := value.(type) { + case int: + number = int64(v) + case int8: + number = int64(v) + case int16: + number = int64(v) + case int32: + number = int64(v) + case int64: + number = v + case uint: + if uint64(v) > uint64(^uint64(0)>>1) { + return symbolicValue{}, fmt.Errorf("value %d is outside the signed i64 range", v) + } + number = int64(v) + case uint8: + number = int64(v) + case uint16: + number = int64(v) + case uint32: + number = int64(v) + case uint64: + if v > uint64(^uint64(0)>>1) { + return symbolicValue{}, fmt.Errorf("value %d is outside the signed i64 range", v) + } + number = int64(v) + case float64: + if v != float64(int64(v)) { + return symbolicValue{}, fmt.Errorf("value %v is not an integer", v) + } + number = int64(v) + case json.Number: + parsed, err := v.Int64() + if err != nil { + return symbolicValue{}, fmt.Errorf("value %q is not an integer", v) + } + number = parsed + default: + return symbolicValue{}, fmt.Errorf("unsupported concrete value %T", value) + } + return typedConstant(number, bits), nil +} func (v symbolicValue) condition() string { if v.boolean { @@ -153,7 +259,7 @@ func (v symbolicValue) condition() string { } return "true" } - return "(not (= " + v.expr + " 0))" + return "(not (= " + v.expr + " " + v.zeroExpr() + "))" } type symbolicState struct { @@ -319,20 +425,26 @@ func executeInstruction(s *symbolicState, in instruction) error { if in.opcode == 0x22 { s.stack = append(s.stack, v) } - case 0x41, 0x42: - s.stack = append(s.stack, constant(in.value)) // i32/i64.const - case 0x45: // i32.eqz + case 0x41: + s.stack = append(s.stack, typedConstant(in.value, 32)) + case 0x42: + s.stack = append(s.stack, typedConstant(in.value, 64)) + case 0x45, 0x50: // i32.eqz / i64.eqz v, err := s.pop() if err != nil { return err } + if (in.opcode == 0x45 && v.bits != 32) || (in.opcode == 0x50 && v.bits != 64) { + return fmt.Errorf("eqz operand has width %d", v.bits) + } var known *bool if v.known != nil { value := *v.known == 0 known = &value } - s.stack = append(s.stack, boolValue("(= "+v.expr+" 0)", known)) - case 0x46, 0x47, 0x48, 0x4a, 0x4c, 0x4e: // eq, ne, lt_s, gt_s, le_s, ge_s + s.stack = append(s.stack, boolValue("(= "+v.expr+" "+v.zeroExpr()+")", known)) + case 0x46, 0x47, 0x48, 0x49, 0x4a, 0x4b, 0x4c, 0x4d, 0x4e, 0x4f, + 0x51, 0x52, 0x53, 0x54, 0x55, 0x56, 0x57, 0x58, 0x59, 0x5a: b, err := s.pop() if err != nil { return err @@ -341,14 +453,20 @@ func executeInstruction(s *symbolicState, in instruction) error { if err != nil { return err } - op := map[byte]string{0x46: "=", 0x47: "distinct", 0x48: "<", 0x4a: ">", 0x4c: "<=", 0x4e: ">="}[in.opcode] + if a.bits == 0 || a.bits != b.bits { + return fmt.Errorf("comparison operands have incompatible widths %d and %d", a.bits, b.bits) + } + op, ok := comparisonOperator(in.opcode) + if !ok { + return fmt.Errorf("unsupported comparison opcode 0x%x", in.opcode) + } var known *bool if a.known != nil && b.known != nil { - value := compare(in.opcode, *a.known, *b.known) + value := compare(in.opcode, *a.known, *b.known, a.bits) known = &value } s.stack = append(s.stack, boolValue("("+op+" "+a.expr+" "+b.expr+")", known)) - case 0x6a, 0x6b, 0x6c: // i32.add/sub/mul + case 0x6a, 0x6b, 0x6c, 0x7c, 0x7d, 0x7e: // i32/i64 add/sub/mul b, err := s.pop() if err != nil { return err @@ -357,19 +475,25 @@ func executeInstruction(s *symbolicState, in instruction) error { if err != nil { return err } - op := map[byte]string{0x6a: "+", 0x6b: "-", 0x6c: "*"}[in.opcode] + bits, ok := arithmeticWidth(in.opcode) + if !ok || a.bits != bits || b.bits != bits { + return fmt.Errorf("arithmetic operands have invalid widths %d and %d", a.bits, b.bits) + } + op := map[byte]string{0x6a: "bvadd", 0x6b: "bvsub", 0x6c: "bvmul", 0x7c: "bvadd", 0x7d: "bvsub", 0x7e: "bvmul"}[in.opcode] if a.known != nil && b.known != nil { + var value int64 switch in.opcode { - case 0x6a: - s.stack = append(s.stack, constant(*a.known+*b.known)) - case 0x6b: - s.stack = append(s.stack, constant(*a.known-*b.known)) + case 0x6a, 0x7c: + value = *a.known + *b.known + case 0x6b, 0x7d: + value = *a.known - *b.known default: - s.stack = append(s.stack, constant(*a.known**b.known)) + value = *a.known * *b.known } - return nil + s.stack = append(s.stack, typedConstant(value, bits)) + } else { + s.stack = append(s.stack, symbolicValue{expr: "(" + op + " " + a.expr + " " + b.expr + ")", bits: bits}) } - s.stack = append(s.stack, symbolicValue{expr: "(" + op + " " + a.expr + " " + b.expr + ")"}) case 0x1a: _, err := s.pop() return err // drop @@ -389,20 +513,68 @@ func boolValue(expr string, value *bool) symbolicValue { } return symbolicValue{expr: expr, boolean: true} } -func compare(op byte, a, b int64) bool { +func comparisonOperator(op byte) (string, bool) { + operators := map[byte]string{ + 0x46: "=", 0x47: "distinct", 0x48: "bvslt", 0x49: "bvult", + 0x4a: "bvsgt", 0x4b: "bvugt", 0x4c: "bvsle", 0x4d: "bvule", + 0x4e: "bvsge", 0x4f: "bvuge", 0x51: "=", 0x52: "distinct", + 0x53: "bvslt", 0x54: "bvult", 0x55: "bvsgt", 0x56: "bvugt", + 0x57: "bvsle", 0x58: "bvule", 0x59: "bvsge", 0x5a: "bvuge", + } + operator, ok := operators[op] + return operator, ok +} + +func arithmeticWidth(op byte) (byte, bool) { switch op { - case 0x46: + case 0x6a, 0x6b, 0x6c: + return 32, true + case 0x7c, 0x7d, 0x7e: + return 64, true + default: + return 0, false + } +} + +func compare(op byte, a, b int64, bits byte) bool { + unsignedA, unsignedB := uint64(a), uint64(b) + if bits < 64 { + mask := (uint64(1) << bits) - 1 + unsignedA &= mask + unsignedB &= mask + } + switch op { + case 0x46, 0x51: return a == b - case 0x47: + case 0x47, 0x52: return a != b - case 0x48: + case 0x48, 0x53: return a < b - case 0x4a: + case 0x49, 0x54: + return unsignedA < unsignedB + case 0x4a, 0x55: return a > b - case 0x4c: + case 0x4b, 0x56: + return unsignedA > unsignedB + case 0x4c, 0x57: return a <= b - default: + case 0x4d, 0x58: + return unsignedA <= unsignedB + case 0x4e, 0x59: return a >= b + default: + return unsignedA >= unsignedB + } +} + +func wasmIntegerWidth(typ byte) (byte, bool) { + switch typ { + case valueI32: + return 32, true + case valueI64: + return 64, true + default: + return 0, false } } @@ -620,7 +792,7 @@ func parseCode(b []byte) ([]byte, []instruction, error) { return nil, nil, fmt.Errorf("invalid wasm locals") } p = q - locals = append(locals, bytesRepeat(b[p], int(n))...) + locals = append(locals, bytes.Repeat([]byte{b[p]}, int(n))...) p++ } body, p, stop, err := parseInstructions(b, p) @@ -632,13 +804,6 @@ func parseCode(b []byte) ([]byte, []instruction, error) { } return locals, body, nil } -func bytesRepeat(v byte, n int) []byte { - r := make([]byte, n) - for i := range r { - r[i] = v - } - return r -} func parseInstructions(b []byte, p int) ([]instruction, int, byte, error) { return parseInstructionsWithBudget(b, p, new(int), 0) } @@ -730,6 +895,7 @@ func SymbolicHandler() http.HandlerFunc { r.Body = http.MaxBytesReader(w, r.Body, maxSymbolicRequestBytes) var input SymbolicInput decoder := json.NewDecoder(r.Body) + decoder.UseNumber() decoder.DisallowUnknownFields() if err := decoder.Decode(&input); err != nil { http.Error(w, fmt.Sprintf("invalid request: %v", err), http.StatusBadRequest) diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index ed571d3..43cceef 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -60,7 +60,7 @@ func TestRun_RejectsInvalidInput(t *testing.T) { func TestSymbolicComparisonConditionPreservesBoolExpression(t *testing.T) { t.Parallel() - state := symbolicState{locals: []symbolicValue{{expr: "arg0"}}} + state := symbolicState{locals: []symbolicValue{{expr: "arg0", bits: 32}}} for _, instruction := range []instruction{ {opcode: 0x20, index: 0}, {opcode: 0x41, value: 0}, @@ -74,11 +74,72 @@ func TestSymbolicComparisonConditionPreservesBoolExpression(t *testing.T) { if err != nil { t.Fatalf("pop() error = %v", err) } - if got, want := condition.condition(), "(= arg0 0)"; got != want { + if got, want := condition.condition(), "(= arg0 (_ bv0 32))"; got != want { t.Errorf("condition() = %q, want %q", got, want) } } +func TestI32ArithmeticWraps(t *testing.T) { + t.Parallel() + + for _, test := range []struct { + name string + opcode byte + a, b int64 + want int64 + }{ + {name: "add", opcode: 0x6a, a: 2147483647, b: 1, want: -2147483648}, + {name: "sub", opcode: 0x6b, a: -2147483648, b: 1, want: 2147483647}, + {name: "mul", opcode: 0x6c, a: 65536, b: 65536, want: 0}, + } { + t.Run(test.name, func(t *testing.T) { + state := symbolicState{stack: []symbolicValue{typedConstant(test.a, 32), typedConstant(test.b, 32)}} + if err := executeInstruction(&state, instruction{opcode: test.opcode}); err != nil { + t.Fatalf("executeInstruction(%#x) error = %v", test.opcode, err) + } + got, err := state.pop() + if err != nil { + t.Fatalf("pop() error = %v", err) + } + if got.known == nil || *got.known != test.want { + t.Errorf("result = %+v, want %d", got, test.want) + } + }) + } +} + +func TestI32ArithmeticSymbolicallyWraps(t *testing.T) { + t.Parallel() + + state := symbolicState{stack: []symbolicValue{{expr: "arg0", bits: 32}, typedConstant(1, 32)}} + if err := executeInstruction(&state, instruction{opcode: 0x6a}); err != nil { + t.Fatalf("executeInstruction(i32.add) error = %v", err) + } + got, err := state.pop() + if err != nil { + t.Fatalf("pop() error = %v", err) + } + if want := "(bvadd arg0 (_ bv1 32))"; got.expr != want { + t.Errorf("symbolic result = %q, want %q", got.expr, want) + } +} + +func TestRun_AcceptsLegacySymbolicInput(t *testing.T) { + t.Parallel() + + result, err := Run(context.Background(), SymbolicInput{ + WasmBinary: wasmReturningI32(42), + Entry: "main", + Args: []any{int32(1)}, + }) + if err != nil { + t.Fatalf("Run() with legacy input error = %v", err) + } + if len(result.Paths) != 1 || result.Paths[0].Output != int32(42) { + t.Errorf("legacy result = %+v, want one path with output 42", result) + } +} + func TestRun_EnforcesGlobalPathLimit(t *testing.T) { t.Parallel() From 0d58e1f685767ce3f22961c09d2fb3d033124f8c Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 21:52:16 +0800 Subject: [PATCH 04/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- cmd/symkerneld/routes_test.go | 38 +++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/cmd/symkerneld/routes_test.go b/cmd/symkerneld/routes_test.go index dbe2bcc..d14680a 100644 --- a/cmd/symkerneld/routes_test.go +++ b/cmd/symkerneld/routes_test.go @@ -4,6 +4,7 @@ import ( "encoding/json" "net/http" "net/http/httptest" + "strings" "testing" ) @@ -64,3 +65,40 @@ func TestRegisterRoutes(t *testing.T) { t.Errorf("POST /v1/verify/symbolic status = %d, want %d; body = %s", srec.Code, http.StatusBadRequest, srec.Body.String()) } } + +func TestRegisterRoutes_SymbolicExecution(t *testing.T) { + // This is a Wasm module which exports main() -> i32 and returns 7. + const module = "AGFzbQEAAAABBQFgAAF/AwIBAAcIAQRtYWluAAAKBgEEAEEHCw==" + + mux := http.NewServeMux() + RegisterRoutes(mux) + + req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", strings.NewReader( + `{"module":"`+module+`","entrypoint":"main","maxDepth":100,"pruneInfeasible":true}`, + )) + rec := httptest.NewRecorder() + mux.ServeHTTP(rec, req) + + if rec.Code != http.StatusOK { + t.Fatalf("POST /v1/verify/symbolic status = %d, want %d; body = %s", rec.Code, http.StatusOK, rec.Body.String()) + } + var response struct { + Paths []struct { + Feasible bool `json:"feasible"` + Constraints []string `json:"constraints"` + Output float64 `json:"output"` + } `json:"paths"` + Explored int `json:"explored"` + Pruned int `json:"pruned"` + } + if err := json.NewDecoder(rec.Body).Decode(&response); err != nil { + t.Fatalf("decode symbolic response: %v", err) + } + if response.Explored != 1 || response.Pruned != 0 || len(response.Paths) != 1 { + t.Fatalf("symbolic response = %+v, want one explored feasible path", response) + } + path := response.Paths[0] + if !path.Feasible || len(path.Constraints) != 0 || path.Output != 7 { + t.Errorf("symbolic path = %+v, want feasible path with output 7", path) + } +} From bbbec19e35ad588ff9e02bda64c424a4c653365e Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 22:46:34 +0800 Subject: [PATCH 05/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- internal/verify/symbolic.go | 65 +++++++++++++++++++++----------- internal/verify/symbolic_test.go | 44 +++++++++++++++++++++ 2 files changed, 86 insertions(+), 23 deletions(-) diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index 0b4186b..0517733 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -8,7 +8,9 @@ import ( "encoding/json" "fmt" "io" + "math" "net/http" + "strconv" "strings" "github.com/WasmAgent/symkernel/internal/z3" @@ -30,17 +32,26 @@ const ( ) // SymbolicInput is the request payload for POST /v1/verify/symbolic. +// Module, Entrypoint, MaxDepth, and PruneInfeasible are the v12 endpoint +// fields. The legacy fields below remain supported so existing Go callers can +// migrate without changing their request construction in one step. When both +// names are supplied, Run requires the module and entrypoint values to agree. type SymbolicInput struct { Module string `json:"module"` Entrypoint string `json:"entrypoint"` MaxDepth int `json:"maxDepth"` PruneInfeasible bool `json:"pruneInfeasible"` - // WasmBinary, Entry, and Args are retained for callers of the original - // symbolic API. Module and Entrypoint are the endpoint field names. + // WasmBinary is the legacy base64-encoded module field. + // Deprecated: use Module. WasmBinary string `json:"wasmBinary,omitempty"` - Entry string `json:"entry,omitempty"` - Args []any `json:"args,omitempty"` + // Entry is the legacy exported function field. + // Deprecated: use Entrypoint. + Entry string `json:"entry,omitempty"` + // Args are concrete legacy function arguments. They are still applied to + // matching parameters when supplied. + // Deprecated: prefer symbolic parameters through the v12 endpoint fields. + Args []any `json:"args,omitempty"` } // SymbolicPath is one terminal path reached by the entrypoint. @@ -211,9 +222,6 @@ func concreteArgument(value any, bits byte) (symbolicValue, error) { case int64: number = v case uint: - if uint64(v) > uint64(^uint64(0)>>1) { - return symbolicValue{}, fmt.Errorf("value %d is outside the signed i64 range", v) - } number = int64(v) case uint8: number = int64(v) @@ -222,21 +230,25 @@ func concreteArgument(value any, bits byte) (symbolicValue, error) { case uint32: number = int64(v) case uint64: - if v > uint64(^uint64(0)>>1) { - return symbolicValue{}, fmt.Errorf("value %d is outside the signed i64 range", v) - } number = int64(v) case float64: - if v != float64(int64(v)) { + const minInt64 = -1 << 63 + if math.IsNaN(v) || math.IsInf(v, 0) || math.Trunc(v) != v || + v < float64(minInt64) || v >= -float64(minInt64) { return symbolicValue{}, fmt.Errorf("value %v is not an integer", v) } number = int64(v) case json.Number: parsed, err := v.Int64() - if err != nil { + if err == nil { + number = parsed + break + } + unsigned, unsignedErr := strconv.ParseUint(string(v), 10, 64) + if unsignedErr != nil { return symbolicValue{}, fmt.Errorf("value %q is not an integer", v) } - number = parsed + number = int64(unsigned) default: return symbolicValue{}, fmt.Errorf("unsupported concrete value %T", value) } @@ -481,16 +493,7 @@ func executeInstruction(s *symbolicState, in instruction) error { } op := map[byte]string{0x6a: "bvadd", 0x6b: "bvsub", 0x6c: "bvmul", 0x7c: "bvadd", 0x7d: "bvsub", 0x7e: "bvmul"}[in.opcode] if a.known != nil && b.known != nil { - var value int64 - switch in.opcode { - case 0x6a, 0x7c: - value = *a.known + *b.known - case 0x6b, 0x7d: - value = *a.known - *b.known - default: - value = *a.known * *b.known - } - s.stack = append(s.stack, typedConstant(value, bits)) + s.stack = append(s.stack, typedConstant(wrappedArithmetic(*a.known, *b.known, in.opcode, bits), bits)) } else { s.stack = append(s.stack, symbolicValue{expr: "(" + op + " " + a.expr + " " + b.expr + ")", bits: bits}) } @@ -503,6 +506,22 @@ func executeInstruction(s *symbolicState, in instruction) error { return nil } +func wrappedArithmetic(a, b int64, opcode, bits byte) int64 { + var value uint64 + switch opcode { + case 0x6a, 0x7c: + value = uint64(a) + uint64(b) + case 0x6b, 0x7d: + value = uint64(a) - uint64(b) + default: + value = uint64(a) * uint64(b) + } + if bits == 32 { + return int64(int32(uint32(value))) + } + return int64(value) +} + func boolValue(expr string, value *bool) symbolicValue { if value != nil { known := int64(0) diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index 43cceef..dc9b4ab 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -124,6 +124,25 @@ func TestI32ArithmeticSymbolicallyWraps(t *testing.T) { } } +func TestI64ArithmeticWraps(t *testing.T) { + t.Parallel() + + state := symbolicState{stack: []symbolicValue{ + typedConstant(9223372036854775807, 64), + typedConstant(1, 64), + }} + if err := executeInstruction(&state, instruction{opcode: 0x7c}); err != nil { + t.Fatalf("executeInstruction(i64.add) error = %v", err) + } + got, err := state.pop() + if err != nil { + t.Fatalf("pop() error = %v", err) + } + if got.known == nil || *got.known != -9223372036854775808 { + t.Errorf("result = %+v, want i64 minimum", got) + } +} + func TestRun_AcceptsLegacySymbolicInput(t *testing.T) { t.Parallel() @@ -140,6 +159,31 @@ func TestRun_AcceptsLegacySymbolicInput(t *testing.T) { } } +func TestConcreteArgumentWrapsToWasmWidth(t *testing.T) { + t.Parallel() + + for _, test := range []struct { + name string + value any + bits byte + want int64 + }{ + {name: "i32 uint overflow", value: uint64(0xffffffff), bits: 32, want: -1}, + {name: "i64 uint overflow", value: ^uint64(0), bits: 64, want: -1}, + {name: "json uint overflow", value: json.Number("18446744073709551615"), bits: 64, want: -1}, + } { + t.Run(test.name, func(t *testing.T) { + got, err := concreteArgument(test.value, test.bits) + if err != nil { + t.Fatalf("concreteArgument() error = %v", err) + } + if got.known == nil || *got.known != test.want { + t.Fatalf("known value = %v, want %d", got.known, test.want) + } + }) + } +} + func TestRun_EnforcesGlobalPathLimit(t *testing.T) { t.Parallel() From f2a9572b281705131202a5d62ccfdefabb85a6f8 Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 23:01:05 +0800 Subject: [PATCH 06/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- internal/verify/symbolic.go | 75 +++++++++++++++++++++++++++++--- internal/verify/symbolic_test.go | 36 +++++++++++++++ 2 files changed, 106 insertions(+), 5 deletions(-) diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index 0517733..0cd0efc 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -638,14 +638,10 @@ func parseExportedFunction(wasm []byte, entrypoint string) (wasmFunction, error) return wasmFunction{}, err } case 2: - count, _, err := readU32(section, 0) + imported, err = parseImportedFunctionCount(section) if err != nil { return wasmFunction{}, err } - if count > maxWasmVectorItems || imported > maxWasmVectorItems-count { - return wasmFunction{}, fmt.Errorf("too many wasm imports") - } - imported += count // imported functions are unsupported below case 3: functions, err = parseU32Vector(section) if err != nil { @@ -686,6 +682,75 @@ func parseExportedFunction(wasm []byte, entrypoint string) (wasmFunction, error) return wasmFunction{params: params, results: results, locals: locals, body: body}, nil } +// parseImportedFunctionCount returns the number of function imports in an +// import section. Only function imports occupy function-index space; tables, +// memories, and globals must still be consumed but do not offset local +// function indices. +func parseImportedFunctionCount(b []byte) (uint32, error) { + count, p, err := readU32(b, 0) + if err != nil { + return 0, err + } + if count > maxWasmVectorItems || int(count) > len(b)-p { + return 0, fmt.Errorf("too many wasm imports") + } + var functions uint32 + for range count { + for range 2 { // module and import names + n, q, err := readU32(b, p) + if err != nil || int(n) > len(b)-q { + return 0, fmt.Errorf("invalid wasm import") + } + p = q + int(n) + } + if p >= len(b) { + return 0, fmt.Errorf("truncated wasm import") + } + switch b[p] { + case 0: // function: type index + functions++ + _, p, err = readU32(b, p+1) + case 1: // table: reference type followed by limits + if p+1 >= len(b) { + return 0, fmt.Errorf("truncated wasm table import") + } + p, err = skipWasmLimits(b, p+2) + case 2: // memory: limits + p, err = skipWasmLimits(b, p+1) + case 3: // global: value type and mutability + if p+2 >= len(b) { + return 0, fmt.Errorf("truncated wasm global import") + } + p += 3 + default: + return 0, fmt.Errorf("invalid wasm import kind") + } + if err != nil { + return 0, err + } + } + if p != len(b) { + return 0, fmt.Errorf("invalid wasm import section") + } + return functions, nil +} + +func skipWasmLimits(b []byte, p int) (int, error) { + flags, p, err := readU32(b, p) + if err != nil { + return 0, err + } + if flags > 1 { + return 0, fmt.Errorf("unsupported wasm limits") + } + _, p, err = readU32(b, p) + if err != nil || flags == 0 { + return p, err + } + _, p, err = readU32(b, p) + return p, err +} + func parseTypes(b []byte) ([][]byte, error) { count, p, err := readU32(b, 0) if err != nil { diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index dc9b4ab..961e66e 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -57,6 +57,32 @@ func TestRun_RejectsInvalidInput(t *testing.T) { } } +func TestRun_HandlesNonFunctionImportsBeforeEntrypoint(t *testing.T) { + t.Parallel() + + for _, test := range []struct { + name string + imports []byte + }{ + {name: "memory", imports: []byte{0x01, 0x01, 'm', 0x03, 'm', 'e', 'm', 0x02, 0x00, 0x01}}, + {name: "table", imports: []byte{0x01, 0x01, 'm', 0x03, 't', 'a', 'b', 0x01, 0x70, 0x00, 0x01}}, + {name: "global", imports: []byte{0x01, 0x01, 'm', 0x01, 'g', 0x03, valueI32, 0x00}}, + } { + t.Run(test.name, func(t *testing.T) { + result, err := Run(context.Background(), SymbolicInput{ + Module: wasmReturningI32WithImports(42, test.imports), + Entrypoint: "main", + }) + if err != nil { + t.Fatalf("Run() error = %v", err) + } + if len(result.Paths) != 1 || result.Paths[0].Output != int32(42) { + t.Errorf("result = %+v, want one path with output 42", result) + } + }) + } +} + func TestSymbolicComparisonConditionPreservesBoolExpression(t *testing.T) { t.Parallel() @@ -321,6 +347,16 @@ func wasmReturningI32(value byte) string { return base64.StdEncoding.EncodeToString(wasm) } +func wasmReturningI32WithImports(value byte, imports []byte) string { + wasm := []byte{0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00} + wasm = append(wasm, wasmSection(1, []byte{0x01, 0x60, 0x00, 0x01, valueI32})...) + wasm = append(wasm, wasmSection(2, imports)...) + wasm = append(wasm, wasmSection(3, []byte{0x01, 0x00})...) + wasm = append(wasm, wasmSection(7, []byte{0x01, 0x04, 'm', 'a', 'i', 'n', 0x00, 0x00})...) + wasm = append(wasm, wasmSection(10, []byte{0x01, 0x04, 0x00, 0x41, value, 0x0b})...) + return base64.StdEncoding.EncodeToString(wasm) +} + func wasmNestedBranch() string { wasm := []byte{ 0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, From 8b2321e05b8b760dbbdca71c6cb6a9e6433ed2ef Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 23:10:32 +0800 Subject: [PATCH 07/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- internal/verify/symbolic.go | 10 +++++++--- internal/verify/symbolic_test.go | 10 ++++++++++ 2 files changed, 17 insertions(+), 3 deletions(-) diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index 0cd0efc..cd65253 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -915,15 +915,19 @@ func parseInstructionsWithBudget(b []byte, p int, instructionCount *int, control return nil, p, 0, fmt.Errorf("truncated if") } p++ - in.then, p, _, err = parseInstructionsWithBudget(b, p, instructionCount, controlDepth+1) + var stop byte + in.then, p, stop, err = parseInstructionsWithBudget(b, p, instructionCount, controlDepth+1) if err != nil { return nil, p, 0, err } - if p > 0 && b[p-1] == 0x05 { - in.otherwise, p, _, err = parseInstructionsWithBudget(b, p, instructionCount, controlDepth+1) + if stop == 0x05 { + in.otherwise, p, stop, err = parseInstructionsWithBudget(b, p, instructionCount, controlDepth+1) if err != nil { return nil, p, 0, err } + if stop != 0x0b { + return nil, p, 0, fmt.Errorf("invalid wasm if: else must end with end opcode") + } } case 0x20, 0x21, 0x22: in.index, p, err = readU32(b, p) diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index 961e66e..4c51774 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -336,6 +336,16 @@ func TestWasmParserRejectsOversizedVectors(t *testing.T) { } } +func TestWasmParserRejectsIfElseTerminatedByElse(t *testing.T) { + t.Parallel() + + // A second else cannot terminate an if's else arm. The final end here is + // for the function body, so accepting this would misassociate delimiters. + if _, _, err := parseCode([]byte{0x00, 0x04, 0x40, 0x05, 0x05, 0x0b}); err == nil { + t.Error("parseCode() error = nil, want invalid if error") + } +} + func wasmReturningI32(value byte) string { wasm := []byte{ 0x00, 0x61, 0x73, 0x6d, 0x01, 0x00, 0x00, 0x00, From 2343e18d84ab5884c087756180720ce0c47e0116 Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sat, 1 Aug 2026 23:43:42 +0800 Subject: [PATCH 08/10] =?UTF-8?q?WIP=20[partial-implement]:=20interrupted?= =?UTF-8?q?=20(deepseek=20implement:=20deepseek=20429=20rate=20limited:=20?= =?UTF-8?q?{"type":"error","error":{"type":"...)=20=E2=80=94=2015:43:42=20?= =?UTF-8?q?UTC?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- deploy/Dockerfile.z3 | 70 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 deploy/Dockerfile.z3 diff --git a/deploy/Dockerfile.z3 b/deploy/Dockerfile.z3 new file mode 100644 index 0000000..21461e5 --- /dev/null +++ b/deploy/Dockerfile.z3 @@ -0,0 +1,70 @@ +# syntax=docker/dockerfile:1.7 + +# Build the Z3 CLI separately so the final image does not need a compiler, +# package manager, or the Z3 development headers. +FROM debian:bookworm-slim AS z3-builder + +ARG BUILD_Z3_FROM_SOURCE=0 +ARG Z3_VERSION=4.13.4 +ENV BUILD_Z3_FROM_SOURCE=${BUILD_Z3_FROM_SOURCE} \ + Z3_VERSION=${Z3_VERSION} + +RUN set -eux; \ + apt-get update; \ + apt-get install -y --no-install-recommends \ + ca-certificates \ + cmake \ + g++ \ + git \ + make \ + python3; \ + install -d /opt/z3/bin /opt/z3/lib; \ + case "${BUILD_Z3_FROM_SOURCE}" in \ + 1|true|TRUE|yes|YES) \ + git clone --depth 1 --branch "z3-${Z3_VERSION}" \ + https://github.com/Z3Prover/z3.git /tmp/z3; \ + cmake -S /tmp/z3 -B /tmp/z3-build \ + -DCMAKE_BUILD_TYPE=Release \ + -DZ3_BUILD_EXECUTABLE=ON \ + -DZ3_BUILD_LIBZ3_SHARED=OFF; \ + cmake --build /tmp/z3-build --parallel; \ + install -D /tmp/z3-build/z3 /opt/z3/bin/z3; \ + find /tmp/z3-build -type f -name 'libz3.a' \ + -exec install -D {} /opt/z3/lib/libz3.a \;; \ + ;; \ + *) \ + apt-get install -y --no-install-recommends z3 libz3-dev; \ + install -D /usr/bin/z3 /opt/z3/bin/z3; \ + find /usr/lib -type f -name 'libz3.so.*' \ + -exec install -D {} /opt/z3/lib/ \;; \ + ;; \ + esac; \ + rm -rf /tmp/z3 /tmp/z3-build /var/lib/apt/lists/* + +# CGO is enabled explicitly because the Z3-enabled application is intended to +# be compatible with the CGO build path, even though the current process +# wrapper invokes the z3 executable rather than linking its C API directly. +FROM golang:1.25-bookworm AS go-builder + +WORKDIR /src +COPY go.mod go.sum ./ +RUN go mod download +COPY . . + +ENV CGO_ENABLED=1 +RUN go build -trimpath -ldflags="-s -w" -o /symkerneld ./cmd/symkerneld + +# distroless/base supplies the dynamic loader and standard C++ runtime needed +# by the distro-package path. Source builds link libz3 statically into z3 and +# therefore only need the executable in that mode. +FROM gcr.io/distroless/base-debian12:nonroot AS final + +COPY --from=go-builder /symkerneld /usr/local/bin/symkerneld +COPY --from=z3-builder /opt/z3/bin/z3 /usr/local/bin/z3 +COPY --from=z3-builder /opt/z3/lib/ /usr/local/lib/ + +ENV SYMKERNEL_ADDR=:8080 \ + LD_LIBRARY_PATH=/usr/local/lib +EXPOSE 8080 + +ENTRYPOINT ["/usr/local/bin/symkerneld"] From cc70e9a0a3078dc4486d7bf8576f9870437df6a8 Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sun, 2 Aug 2026 00:55:05 +0800 Subject: [PATCH 09/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- deploy/Dockerfile.z3 | 70 -------------------------------- internal/verify/symbolic.go | 6 +++ internal/verify/symbolic_test.go | 17 ++++++++ 3 files changed, 23 insertions(+), 70 deletions(-) delete mode 100644 deploy/Dockerfile.z3 diff --git a/deploy/Dockerfile.z3 b/deploy/Dockerfile.z3 deleted file mode 100644 index 21461e5..0000000 --- a/deploy/Dockerfile.z3 +++ /dev/null @@ -1,70 +0,0 @@ -# syntax=docker/dockerfile:1.7 - -# Build the Z3 CLI separately so the final image does not need a compiler, -# package manager, or the Z3 development headers. -FROM debian:bookworm-slim AS z3-builder - -ARG BUILD_Z3_FROM_SOURCE=0 -ARG Z3_VERSION=4.13.4 -ENV BUILD_Z3_FROM_SOURCE=${BUILD_Z3_FROM_SOURCE} \ - Z3_VERSION=${Z3_VERSION} - -RUN set -eux; \ - apt-get update; \ - apt-get install -y --no-install-recommends \ - ca-certificates \ - cmake \ - g++ \ - git \ - make \ - python3; \ - install -d /opt/z3/bin /opt/z3/lib; \ - case "${BUILD_Z3_FROM_SOURCE}" in \ - 1|true|TRUE|yes|YES) \ - git clone --depth 1 --branch "z3-${Z3_VERSION}" \ - https://github.com/Z3Prover/z3.git /tmp/z3; \ - cmake -S /tmp/z3 -B /tmp/z3-build \ - -DCMAKE_BUILD_TYPE=Release \ - -DZ3_BUILD_EXECUTABLE=ON \ - -DZ3_BUILD_LIBZ3_SHARED=OFF; \ - cmake --build /tmp/z3-build --parallel; \ - install -D /tmp/z3-build/z3 /opt/z3/bin/z3; \ - find /tmp/z3-build -type f -name 'libz3.a' \ - -exec install -D {} /opt/z3/lib/libz3.a \;; \ - ;; \ - *) \ - apt-get install -y --no-install-recommends z3 libz3-dev; \ - install -D /usr/bin/z3 /opt/z3/bin/z3; \ - find /usr/lib -type f -name 'libz3.so.*' \ - -exec install -D {} /opt/z3/lib/ \;; \ - ;; \ - esac; \ - rm -rf /tmp/z3 /tmp/z3-build /var/lib/apt/lists/* - -# CGO is enabled explicitly because the Z3-enabled application is intended to -# be compatible with the CGO build path, even though the current process -# wrapper invokes the z3 executable rather than linking its C API directly. -FROM golang:1.25-bookworm AS go-builder - -WORKDIR /src -COPY go.mod go.sum ./ -RUN go mod download -COPY . . - -ENV CGO_ENABLED=1 -RUN go build -trimpath -ldflags="-s -w" -o /symkerneld ./cmd/symkerneld - -# distroless/base supplies the dynamic loader and standard C++ runtime needed -# by the distro-package path. Source builds link libz3 statically into z3 and -# therefore only need the executable in that mode. -FROM gcr.io/distroless/base-debian12:nonroot AS final - -COPY --from=go-builder /symkerneld /usr/local/bin/symkerneld -COPY --from=z3-builder /opt/z3/bin/z3 /usr/local/bin/z3 -COPY --from=z3-builder /opt/z3/lib/ /usr/local/lib/ - -ENV SYMKERNEL_ADDR=:8080 \ - LD_LIBRARY_PATH=/usr/local/lib -EXPOSE 8080 - -ENTRYPOINT ["/usr/local/bin/symkerneld"] diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index cd65253..bfda7d6 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -6,6 +6,7 @@ import ( "context" "encoding/base64" "encoding/json" + "errors" "fmt" "io" "math" @@ -31,6 +32,11 @@ const ( maxWasmControlDepth = 256 ) +// ErrNotImplemented is retained for source compatibility with callers of the +// original symbolic-verification scaffold. Run is implemented and no longer +// returns this sentinel. +var ErrNotImplemented = errors.New("symbolic verification not implemented") + // SymbolicInput is the request payload for POST /v1/verify/symbolic. // Module, Entrypoint, MaxDepth, and PruneInfeasible are the v12 endpoint // fields. The legacy fields below remain supported so existing Go callers can diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index 4c51774..b37da9b 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -305,6 +305,23 @@ func TestSymbolicHandler_RejectsInvalidRequest(t *testing.T) { } } +func TestSymbolicHandler_RejectsNullAndEmptyObject(t *testing.T) { + t.Parallel() + + for _, body := range []string{"null", "{}"} { + t.Run(body, func(t *testing.T) { + req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", strings.NewReader(body)) + rec := httptest.NewRecorder() + + SymbolicHandler().ServeHTTP(rec, req) + + if rec.Code != http.StatusBadRequest { + t.Errorf("status = %d, want %d; body = %s", rec.Code, http.StatusBadRequest, rec.Body.String()) + } + }) + } +} + func TestSymbolicHandler_RejectsOversizedRequest(t *testing.T) { t.Parallel() From e72ac6988dbb26cfbdd07488ff0c845feea85235 Mon Sep 17 00:00:00 2001 From: claude-bot-go Date: Sun, 2 Aug 2026 01:02:36 +0800 Subject: [PATCH 10/10] =?UTF-8?q?Fix=20#287:=20[milestone=20Milestone=2012?= =?UTF-8?q?]=20`POST=20/v1/verify/symbolic`=20=E2=80=94=20Symbolic=20WASM?= =?UTF-8?q?=20execution=20endpoint:=20`{"module":"bas...?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- internal/verify/symbolic.go | 87 +++++++++++++++++++++++++++----- internal/verify/symbolic_test.go | 14 +++-- 2 files changed, 85 insertions(+), 16 deletions(-) diff --git a/internal/verify/symbolic.go b/internal/verify/symbolic.go index bfda7d6..dcef358 100644 --- a/internal/verify/symbolic.go +++ b/internal/verify/symbolic.go @@ -62,10 +62,18 @@ type SymbolicInput struct { // SymbolicPath is one terminal path reached by the entrypoint. type SymbolicPath struct { - ID string `json:"id"` - Feasible bool `json:"feasible"` - Constraints []string `json:"constraints"` - Output any `json:"output"` + // Constraints is the SMT-LIB assertions guarding this path. It remains a + // string for compatibility with callers that pass it to SolveConstraintsCtx. + Constraints string `json:"constraints"` + // Model is a satisfying assignment for Constraints keyed by symbol. It is + // retained for compatibility with the original symbolic API. + Model map[string]any `json:"model"` + + ID string `json:"id"` + Feasible bool `json:"feasible"` + Output any `json:"output"` + + constraints []string } // SymbolicResult is the response payload for symbolic verification. @@ -168,7 +176,7 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { } paths := make([]SymbolicPath, 0, len(states)) for _, state := range states { - feasible, err := exec.feasible(state.constraints) + feasible, pathModel, err := exec.feasibility(state.constraints) if err != nil { return SymbolicResult{}, err } @@ -180,13 +188,25 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) { return SymbolicResult{}, fmt.Errorf("entrypoint %q did not produce its declared results", entrypoint) } paths = append(paths, SymbolicPath{ - ID: uuid.NewString(), Feasible: feasible, Constraints: state.constraints, - Output: state.output(fn.results), + ID: uuid.NewString(), + Feasible: feasible, + Constraints: smt2Assertions(state.constraints), + Model: pathModel, + Output: state.output(fn.results), + constraints: append([]string(nil), state.constraints...), }) } return SymbolicResult{Paths: paths, Explored: exec.explored, Pruned: exec.pruned, DecisionID: uuid.NewString()}, nil } +func smt2Assertions(constraints []string) string { + var b strings.Builder + for _, constraint := range constraints { + fmt.Fprintf(&b, "(assert %s)\n", constraint) + } + return b.String() +} + type symbolicValue struct { expr string known *int64 @@ -403,8 +423,13 @@ func (e *executor) run(program []instruction, states []symbolicState) ([]symboli } func (e *executor) feasible(constraints []string) (bool, error) { + feasible, _, err := e.feasibility(constraints) + return feasible, err +} + +func (e *executor) feasibility(constraints []string) (bool, map[string]any, error) { if len(constraints) == 0 { - return true, nil + return true, nil, nil } var b strings.Builder for _, c := range constraints { @@ -412,15 +437,15 @@ func (e *executor) feasible(constraints []string) (bool, error) { } solution, err := z3.SolveConstraintsCtx(e.ctx, b.String(), e.model) if err != nil { - return false, fmt.Errorf("check path feasibility: %w", err) + return false, nil, fmt.Errorf("check path feasibility: %w", err) } switch solution.Sat { case "sat": - return true, nil + return true, solution.Model, nil case "unsat": - return false, nil + return false, nil, nil default: - return false, fmt.Errorf("check path feasibility: z3 returned %q", solution.Sat) + return false, nil, fmt.Errorf("check path feasibility: z3 returned %q", solution.Sat) } } @@ -1005,6 +1030,42 @@ func SymbolicHandler() http.HandlerFunc { return } w.Header().Set("Content-Type", "application/json") - _ = json.NewEncoder(w).Encode(result) + _ = json.NewEncoder(w).Encode(symbolicHTTPResponse(result)) + } +} + +// symbolicHTTPResponse keeps the v12 HTTP contract independent of the +// long-standing Go SymbolicPath API. In particular, the endpoint returns one +// expression per constraints array element while Go callers retain the single +// SMT-LIB constraint string required by existing solver integrations. +type symbolicHTTPPath struct { + ID string `json:"id"` + Feasible bool `json:"feasible"` + Constraints []string `json:"constraints"` + Output any `json:"output"` +} + +type symbolicHTTPResult struct { + Paths []symbolicHTTPPath `json:"paths"` + Explored int `json:"explored"` + Pruned int `json:"pruned"` + DecisionID string `json:"decision_id"` +} + +func symbolicHTTPResponse(result SymbolicResult) symbolicHTTPResult { + paths := make([]symbolicHTTPPath, len(result.Paths)) + for i, path := range result.Paths { + paths[i] = symbolicHTTPPath{ + ID: path.ID, + Feasible: path.Feasible, + Constraints: append([]string(nil), path.constraints...), + Output: path.Output, + } + } + return symbolicHTTPResult{ + Paths: paths, + Explored: result.Explored, + Pruned: result.Pruned, + DecisionID: result.DecisionID, } } diff --git a/internal/verify/symbolic_test.go b/internal/verify/symbolic_test.go index b37da9b..a2573b3 100644 --- a/internal/verify/symbolic_test.go +++ b/internal/verify/symbolic_test.go @@ -30,9 +30,12 @@ func TestRun_ExecutesEntrypoint(t *testing.T) { t.Fatalf("paths = %d, want 1", len(result.Paths)) } path := result.Paths[0] - if !path.Feasible || len(path.Constraints) != 0 || path.Output != int32(42) { + if !path.Feasible || path.Constraints != "" || path.Output != int32(42) { t.Errorf("path = %+v, want feasible empty-constraint path with output 42", path) } + if path.Model != nil { + t.Errorf("path.Model = %v, want nil for a function with no symbolic parameters", path.Model) + } if _, err := uuid.Parse(path.ID); err != nil { t.Errorf("path ID = %q is not a UUID: %v", path.ID, err) } @@ -278,11 +281,16 @@ func TestSymbolicHandler(t *testing.T) { if contentType := rec.Header().Get("Content-Type"); contentType != "application/json" { t.Errorf("Content-Type = %q, want application/json", contentType) } - var result SymbolicResult + var result struct { + Paths []struct { + Constraints []string `json:"constraints"` + Output any `json:"output"` + } `json:"paths"` + } if err := json.NewDecoder(rec.Body).Decode(&result); err != nil { t.Fatalf("decode response: %v", err) } - if len(result.Paths) != 1 || result.Paths[0].Output != float64(7) { + if len(result.Paths) != 1 || len(result.Paths[0].Constraints) != 0 || result.Paths[0].Output != float64(7) { t.Errorf("response = %+v, want one path with output 7", result) } }