mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 01:01:19 +00:00
Code Activity

Fix unsafe.Pointer usage in Go propagator - use uintptr_t for cgo.Handle

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-23 01:09:07 +00:00
parent 0de7af9112
commit d5030dfe30
3 changed files with 50 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/api/go/propagator.go
View file

@ -2,9 +2,10 @@ package z3
/*
#include "z3.h"
#include <stdint.h>
// 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
}

38
src/api/go/propagator_bridge.c
View file

@ -1,56 +1,60 @@
#include "z3.h"
#include "_cgo_export.h"
#include <stdint.h>
/* 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);
}

47
src/api/go/propagator_callbacks.go
View file

@ -2,6 +2,7 @@ package z3
/*
#include "z3.h"
#include <stdint.h>
*/
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)