Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions cmd/symkerneld/routes.go
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ func RegisterRoutes(mux *http.ServeMux) {
mux.Handle("POST /v1/verify/cel", cellib.Handler())
mux.Handle("POST /v1/verify/z3", verify.Handler(&verify.Z3Solver{}))
mux.Handle("POST /v1/verify/criterion", criterion.Handler())
mux.Handle("POST /v1/verify/symbolic", verify.SymbolicHandler())

orchestrator.NewRouter().RegisterRoutes(mux)
audit.New().RegisterRoutes(mux)
Expand Down
18 changes: 18 additions & 0 deletions cmd/symkerneld/routes_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -54,4 +54,22 @@ func TestRegisterRoutes(t *testing.T) {
if zrec.Code == http.StatusNotFound {
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.
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")
}
}
29 changes: 29 additions & 0 deletions internal/verify/symbolic.go
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,9 @@ package verify

import (
"context"
"encoding/json"
"errors"
"net/http"

"github.com/google/uuid"
)
Expand Down Expand Up @@ -62,3 +64,30 @@ func Run(ctx context.Context, in SymbolicInput) (SymbolicResult, error) {
_ = 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.
func SymbolicHandler() http.HandlerFunc {
return func(w http.ResponseWriter, _ *http.Request) {
w.Header().Set("Content-Type", "application/json")
w.WriteHeader(http.StatusOK)
_ = json.NewEncoder(w).Encode(symbolicPlaceholderResponse{
Message: "Symbolic execution endpoint placeholder",
})
}
}
58 changes: 58 additions & 0 deletions internal/verify/symbolic_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,11 @@ package verify

import (
"context"
"encoding/json"
"errors"
"net/http"
"net/http/httptest"
"strings"
"testing"

"github.com/google/uuid"
Expand Down Expand Up @@ -97,3 +101,57 @@ func TestRun_DecisionIDIsUnique(t *testing.T) {
t.Fatalf("DecisionIDs collided: %s", a.DecisionID)
}
}

// 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) {
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":[]}}`
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)

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

var resp symbolicPlaceholderResponse
if err := json.NewDecoder(rec.Body).Decode(&resp); err != nil {
t.Fatalf("decode response: %v; body = %s", err, rec.Body.String())
}
const want = "Symbolic execution endpoint placeholder"
if resp.Message != want {
t.Errorf("message = %q, want %q", resp.Message, want)
}
}

// 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) {
t.Parallel()

handler := SymbolicHandler()

req := httptest.NewRequest(http.MethodPost, "/v1/verify/symbolic", nil)
rec := httptest.NewRecorder()

handler.ServeHTTP(rec, req)

if rec.Code != http.StatusOK {
t.Fatalf("status = %d, want %d; body = %s", rec.Code, http.StatusOK, rec.Body.String())
}
}