From d5030dfe3019d8ad701985642d242cd06935326a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Mon, 23 Feb 2026 01:09:07 +0000 Subject: [PATCH] Fix unsafe.Pointer usage in Go propagator - use uintptr_t for cgo.Handle Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/go/propagator.go | 12 ++++---- src/api/go/propagator_bridge.c | 38 +++++++++++++----------- src/api/go/propagator_callbacks.go | 47 +++++++++++++++--------------- 3 files changed, 50 insertions(+), 47 deletions(-) diff --git a/src/api/go/propagator.go b/src/api/go/propagator.go index b15db31b2..a2a230dde 100644 --- a/src/api/go/propagator.go +++ b/src/api/go/propagator.go @@ -2,9 +2,10 @@ package z3 /* #include "z3.h" +#include // Declarations for C helper functions defined in propagator_bridge.c -extern void z3go_solver_propagate_init(Z3_context ctx, Z3_solver s, void* user_ctx); +extern void z3go_solver_propagate_init(Z3_context ctx, Z3_solver s, uintptr_t user_ctx); extern void z3go_solver_propagate_fixed(Z3_context ctx, Z3_solver s); extern void z3go_solver_propagate_final(Z3_context ctx, Z3_solver s); extern void z3go_solver_propagate_eq(Z3_context ctx, Z3_solver s); @@ -12,12 +13,11 @@ extern void z3go_solver_propagate_diseq(Z3_context ctx, Z3_solver s); extern void z3go_solver_propagate_created(Z3_context ctx, Z3_solver s); extern void z3go_solver_propagate_decide(Z3_context ctx, Z3_solver s); extern void z3go_solver_propagate_on_binding(Z3_context ctx, Z3_solver s); -extern void z3go_solver_register_on_clause(Z3_context ctx, Z3_solver s, void* user_ctx); +extern void z3go_solver_register_on_clause(Z3_context ctx, Z3_solver s, uintptr_t user_ctx); */ import "C" import ( "runtime/cgo" - "unsafe" ) // UserPropagator implements a custom theory propagator for Z3. @@ -99,8 +99,7 @@ func newUserPropagator(ctx *Context, solver *Solver, iface UserPropagatorCallbac iface: iface, } p.handle = cgo.NewHandle(p) - voidCtx := unsafe.Pointer(uintptr(p.handle)) - C.z3go_solver_propagate_init(ctx.ptr, solver.ptr, voidCtx) + C.z3go_solver_propagate_init(ctx.ptr, solver.ptr, C.uintptr_t(p.handle)) return p } @@ -266,8 +265,7 @@ func (s *Solver) NewOnClause(handler OnClauseHandler) *OnClause { handler: handler, } oc.handle = cgo.NewHandle(oc) - voidCtx := unsafe.Pointer(uintptr(oc.handle)) - C.z3go_solver_register_on_clause(s.ctx.ptr, s.ptr, voidCtx) + C.z3go_solver_register_on_clause(s.ctx.ptr, s.ptr, C.uintptr_t(oc.handle)) return oc } diff --git a/src/api/go/propagator_bridge.c b/src/api/go/propagator_bridge.c index 1e4b1d8ee..b3c6c215e 100644 --- a/src/api/go/propagator_bridge.c +++ b/src/api/go/propagator_bridge.c @@ -1,56 +1,60 @@ #include "z3.h" #include "_cgo_export.h" +#include -/* Bridge functions that adapt C callback signatures to exported Go functions */ +/* Bridge functions that adapt C callback signatures to exported Go functions. + * The user context (void*) is stored/received as uintptr_t to avoid unsafe pointer + * conversion warnings in Go. */ static void propagator_push_bridge(void* ctx, Z3_solver_callback cb) { - goPushCb(ctx, cb); + goPushCb((uintptr_t)ctx, cb); } static void propagator_pop_bridge(void* ctx, Z3_solver_callback cb, unsigned num_scopes) { - goPopCb(ctx, cb, num_scopes); + goPopCb((uintptr_t)ctx, cb, num_scopes); } static void* propagator_fresh_bridge(void* ctx, Z3_context new_context) { - return goFreshCb(ctx, new_context); + return (void*)goFreshCb((uintptr_t)ctx, new_context); } static void propagator_fixed_bridge(void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value) { - goFixedCb(ctx, cb, t, value); + goFixedCb((uintptr_t)ctx, cb, t, value); } static void propagator_eq_bridge(void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t) { - goEqCb(ctx, cb, s, t); + goEqCb((uintptr_t)ctx, cb, s, t); } static void propagator_diseq_bridge(void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t) { - goDiseqCb(ctx, cb, s, t); + goDiseqCb((uintptr_t)ctx, cb, s, t); } static void propagator_final_bridge(void* ctx, Z3_solver_callback cb) { - goFinalCb(ctx, cb); + goFinalCb((uintptr_t)ctx, cb); } static void propagator_created_bridge(void* ctx, Z3_solver_callback cb, Z3_ast t) { - goCreatedCb(ctx, cb, t); + goCreatedCb((uintptr_t)ctx, cb, t); } static void propagator_decide_bridge(void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase) { - goDecideCb(ctx, cb, t, idx, phase); + goDecideCb((uintptr_t)ctx, cb, t, idx, phase); } static bool propagator_on_binding_bridge(void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst) { - return goOnBindingCb(ctx, cb, q, inst); + return goOnBindingCb((uintptr_t)ctx, cb, q, inst); } static void on_clause_bridge(void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals) { - goOnClauseCb(ctx, proof_hint, n, (unsigned*)deps, literals); + goOnClauseCb((uintptr_t)ctx, proof_hint, n, (unsigned*)deps, literals); } -/* C helper functions that Go calls to register callbacks */ +/* C helper functions that Go calls to register callbacks. + * These take uintptr_t for the user context and cast it to void* internally. */ -void z3go_solver_propagate_init(Z3_context ctx, Z3_solver s, void* user_ctx) { - Z3_solver_propagate_init(ctx, s, user_ctx, +void z3go_solver_propagate_init(Z3_context ctx, Z3_solver s, uintptr_t user_ctx) { + Z3_solver_propagate_init(ctx, s, (void*)user_ctx, propagator_push_bridge, propagator_pop_bridge, propagator_fresh_bridge); @@ -84,6 +88,6 @@ void z3go_solver_propagate_on_binding(Z3_context ctx, Z3_solver s) { Z3_solver_propagate_on_binding(ctx, s, propagator_on_binding_bridge); } -void z3go_solver_register_on_clause(Z3_context ctx, Z3_solver s, void* user_ctx) { - Z3_solver_register_on_clause(ctx, s, user_ctx, on_clause_bridge); +void z3go_solver_register_on_clause(Z3_context ctx, Z3_solver s, uintptr_t user_ctx) { + Z3_solver_register_on_clause(ctx, s, (void*)user_ctx, on_clause_bridge); } diff --git a/src/api/go/propagator_callbacks.go b/src/api/go/propagator_callbacks.go index 2966d54ea..d620165a8 100644 --- a/src/api/go/propagator_callbacks.go +++ b/src/api/go/propagator_callbacks.go @@ -2,6 +2,7 @@ package z3 /* #include "z3.h" +#include */ import "C" import ( @@ -12,8 +13,8 @@ import ( // goPushCb is exported to C as a callback for Z3_push_eh. // //export goPushCb -func goPushCb(ctx unsafe.Pointer, cb C.Z3_solver_callback) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goPushCb(ctx C.uintptr_t, cb C.Z3_solver_callback) { + p := cgo.Handle(ctx).Value().(*UserPropagator) old := p.cb p.cb = cb defer func() { p.cb = old }() @@ -23,8 +24,8 @@ func goPushCb(ctx unsafe.Pointer, cb C.Z3_solver_callback) { // goPopCb is exported to C as a callback for Z3_pop_eh. // //export goPopCb -func goPopCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, numScopes C.uint) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goPopCb(ctx C.uintptr_t, cb C.Z3_solver_callback, numScopes C.uint) { + p := cgo.Handle(ctx).Value().(*UserPropagator) old := p.cb p.cb = cb defer func() { p.cb = old }() @@ -34,8 +35,8 @@ func goPopCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, numScopes C.uint) { // goFreshCb is exported to C as a callback for Z3_fresh_eh. // //export goFreshCb -func goFreshCb(ctx unsafe.Pointer, newContext C.Z3_context) unsafe.Pointer { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goFreshCb(ctx C.uintptr_t, newContext C.Z3_context) C.uintptr_t { + p := cgo.Handle(ctx).Value().(*UserPropagator) freshCtx := &Context{ptr: newContext} freshIface := p.iface.Fresh(freshCtx) freshProp := &UserPropagator{ @@ -43,14 +44,14 @@ func goFreshCb(ctx unsafe.Pointer, newContext C.Z3_context) unsafe.Pointer { iface: freshIface, } freshProp.handle = cgo.NewHandle(freshProp) - return unsafe.Pointer(uintptr(freshProp.handle)) + return C.uintptr_t(freshProp.handle) } // goFixedCb is exported to C as a callback for Z3_fixed_eh. // //export goFixedCb -func goFixedCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, t C.Z3_ast, value C.Z3_ast) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goFixedCb(ctx C.uintptr_t, cb C.Z3_solver_callback, t C.Z3_ast, value C.Z3_ast) { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(FixedHandler); ok { old := p.cb p.cb = cb @@ -62,8 +63,8 @@ func goFixedCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, t C.Z3_ast, value C. // goEqCb is exported to C as a callback for Z3_eq_eh (equality). // //export goEqCb -func goEqCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goEqCb(ctx C.uintptr_t, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(EqHandler); ok { old := p.cb p.cb = cb @@ -75,8 +76,8 @@ func goEqCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) // goDiseqCb is exported to C as a callback for Z3_eq_eh (disequality). // //export goDiseqCb -func goDiseqCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goDiseqCb(ctx C.uintptr_t, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_ast) { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(DiseqHandler); ok { old := p.cb p.cb = cb @@ -88,8 +89,8 @@ func goDiseqCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, s C.Z3_ast, t C.Z3_a // goFinalCb is exported to C as a callback for Z3_final_eh. // //export goFinalCb -func goFinalCb(ctx unsafe.Pointer, cb C.Z3_solver_callback) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goFinalCb(ctx C.uintptr_t, cb C.Z3_solver_callback) { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(FinalHandler); ok { old := p.cb p.cb = cb @@ -101,8 +102,8 @@ func goFinalCb(ctx unsafe.Pointer, cb C.Z3_solver_callback) { // goCreatedCb is exported to C as a callback for Z3_created_eh. // //export goCreatedCb -func goCreatedCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, t C.Z3_ast) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goCreatedCb(ctx C.uintptr_t, cb C.Z3_solver_callback, t C.Z3_ast) { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(CreatedHandler); ok { old := p.cb p.cb = cb @@ -114,8 +115,8 @@ func goCreatedCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, t C.Z3_ast) { // goDecideCb is exported to C as a callback for Z3_decide_eh. // //export goDecideCb -func goDecideCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, t C.Z3_ast, idx C.uint, phase C.bool) { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goDecideCb(ctx C.uintptr_t, cb C.Z3_solver_callback, t C.Z3_ast, idx C.uint, phase C.bool) { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(DecideHandler); ok { old := p.cb p.cb = cb @@ -127,8 +128,8 @@ func goDecideCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, t C.Z3_ast, idx C.u // goOnBindingCb is exported to C as a callback for Z3_on_binding_eh. // //export goOnBindingCb -func goOnBindingCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, q C.Z3_ast, inst C.Z3_ast) C.bool { - p := cgo.Handle(uintptr(ctx)).Value().(*UserPropagator) +func goOnBindingCb(ctx C.uintptr_t, cb C.Z3_solver_callback, q C.Z3_ast, inst C.Z3_ast) C.bool { + p := cgo.Handle(ctx).Value().(*UserPropagator) if h, ok := p.iface.(OnBindingHandler); ok { old := p.cb p.cb = cb @@ -144,8 +145,8 @@ func goOnBindingCb(ctx unsafe.Pointer, cb C.Z3_solver_callback, q C.Z3_ast, inst // goOnClauseCb is exported to C as a callback for Z3_on_clause_eh. // //export goOnClauseCb -func goOnClauseCb(ctx unsafe.Pointer, proofHint C.Z3_ast, n C.uint, deps *C.uint, literals C.Z3_ast_vector) { - oc := cgo.Handle(uintptr(ctx)).Value().(*OnClause) +func goOnClauseCb(ctx C.uintptr_t, proofHint C.Z3_ast, n C.uint, deps *C.uint, literals C.Z3_ast_vector) { + oc := cgo.Handle(ctx).Value().(*OnClause) var ph *Expr if proofHint != nil { ph = newExpr(oc.ctx, proofHint)