Skip to content

Function pointer - #178

Open
hei411 wants to merge 16 commits into
mainfrom
heili/func-pointer
Open

Function pointer#178
hei411 wants to merge 16 commits into
mainfrom
heili/func-pointer

Conversation

@hei411

@hei411 hei411 commented Jul 22, 2026

Copy link
Copy Markdown
Contributor

Adding function pointers to PAL
We axiomatize the behavior of function pointer in pulse/Pulse.Lib.C.FuncPtr.fsti, e.g.

  • valid and is_valid describes the spec of the function pointer
  • weaken allows us to relax the spec
  • call applies the function pointer with arguments

Future work:

  • comparing function pointers
  • function pointers that are recursive by calling itself
  • providing an implementation of the axiomatized interface

@hei411
hei411 marked this pull request as draft July 22, 2026 18:55
@hei411
hei411 force-pushed the heili/func-pointer branch from c6fa059 to cf6754e Compare July 23, 2026 21:05
@hei411
hei411 marked this pull request as ready for review July 23, 2026 22:40
gebner
gebner requested changes Jul 23, 2026
View reviewed changes
Comment thread src/pass/emit.rs Outdated
@hei411
hei411 marked this pull request as draft July 23, 2026 22:46
hei411 and others added 8 commits July 24, 2026 05:30
@hei411
Function pointer support (squashed)
52d3dcd 
Squashed 22 commits from heili/func-pointer for a clean rebase onto main.
Adds func_pointer/ examples, Pulse.Lib.C.FuncPtr.fsti, and emitter/IR
support for function pointers (typedefs, args, null, is_valid, struct
fields, _old on pointer args).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 89e3053b-4388-4455-895e-3f3b624594f1
@hei411
Add function pointer examples for array
7160c47
@hei411
Move func-pointer directory to tests
3cfd80c
@hei411
reformatting func pointer example
ca99df6
@hei411
simplify func pointer annotations
cd5000a
@hei411
more examples for func pointer
fc7aa41
@hei411
Make function pointers divergence-aware
c4044dd 
PAL now emits every function as `divergent fn` (stt_div) unless `_total`.
Extend the FuncPtr library, emitter, and tests so function pointers track
whether their target may diverge.

- fsti: add a `div: bool` bit to valid/is_valid; add of_fn_div/
  of_fn_div_valid and call_div; extend weaken with a `div ==> div'`
  refinement (allows total->divergent, forbids the reverse).
- emit.rs: pick of_fn vs of_fn_div by target totality, emit the __fp
  wrapper as `fn`/`divergent fn` by the function's totality, and emit
  call vs call_div by the enclosing body's totality.
- func_pointer.c: migrate all annotations to the div-aware API; add
  add_t (_total), use_total_fp (total pointer), and weaken_total_to_div
  (total->divergent weakening); refresh comments.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 89e3053b-4388-4455-895e-3f3b624594f1
@hei411
Remove fn_total_map, since the totality can be inferred from the envi…
e35e276 
…ronment
@hei411
hei411 force-pushed the heili/func-pointer branch from 5a2cc31 to e35e276 Compare July 24, 2026 05:38
@hei411
hei411 marked this pull request as ready for review July 24, 2026 05:52
gebner
gebner requested changes Jul 27, 2026
View reviewed changes

@gebner gebner left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The basics look great, thank you!

I think we went a bit too fast on some more advanced features (like the ptr_arg_cb test). Let's shelve those for now, and do more design work so that they work more smoothly.

Function pointers are a tangential feature in C. Supporting function pointers shouldn't change or complicate the way we translate every function. We should only pay the price when they're used, also in the PAL emit module.

Comment thread src/pass/emit.rs
Comment thread src/pass/emit.rs Outdated
Comment thread src/pass/emit.rs Outdated
Comment thread src/pass/emit.rs Outdated
Comment thread src/pass/emit.rs Outdated
hei411 and others added 7 commits July 28, 2026 00:04
@hei411
Emit fnptr triple in a separate Funcptr_<g> module
dd27890 
Move the function-pointer triple (func_<g>_pre / _post / __fp) out of the
function's own Func_<g> module into a dedicated Funcptr_<g> module.

- Add funcptr_module_name(g) helper and register the triple names under
  Funcptr_<g> in build_fn_module_map so emit_name auto-qualifies all
  triple and spec references (of_fn, is_valid, etc.). The base func_<g>
  stays in Func_<g>.
- emit_multifile now emits the triple as a standalone PendingModule
  (.fst + .fsti); the wrapper body qualifies Func_<g>.func_<g>.
- Re-point the hand-written inline-Pulse escape hatches in
  test/func_pointer/func_pointer.c from Func_<g>.func_<g>_{pre,post,__fp}
  to Funcptr_<g>.*.

Gating is unchanged: only address-taken functions get a triple.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
@hei411
Recover fnptr pre/post via pre_of/post_of instead of generated defs
74ed5e0 
Stop generating named `func_<g>_pre`/`_post` slprops. Instead inline the
pre/post directly into the `func_<g>__fp` wrapper's requires/ensures and
recover them generically from the wrapper's type via new library
projectors.

- pulse/Pulse.Lib.C.FuncPtr.fsti: add `[@@pulse_eager_unfold] unfold let`
  projectors `pre_of`/`post_of` (over `stt_div`) and `pre_of_tot`/
  `post_of_tot` (over `stt`). `unfold` is required so they reduce in F*'s
  SMT VCs, not just Pulse slprop matching.
- src/pass/emit.rs: `emit_fnptr_spec_core`/`emit_fnptr_triple` inline the
  pre/post into the wrapper (no more `func_<g>_pre`/`_post` defs);
  `emit_of_fn` uses `of_fn[_div] (pre_of[_tot] ..) (post_of[_tot] ..)
  func_<g>__fp`, choosing the `_tot` variant when the function is `_total`.
  Drop the now-dead `_pre`/`_post` module-map entries and name helpers.
- test/func_pointer/func_pointer.c: rewrite hand-written `_pre`/`_post`
  references to the projector form (`_tot` for the total `add_t`); switch
  four `Reassign_join_spec` identity coercions from explicit `rewrite` to
  empty bodies, which succeed via `pulse_eager_unfold`.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
@hei411
Remove ad-hoc __pal_arrwr array_write trick; disable fnptr-array tests
30c4d08 
The emitter special-cased storing a function pointer into an array slot by
let-binding the value to a temporary (__pal_arrwr) before array_write, keeping
the array spec update over a small variable so the array_spec_upd_* SMTPats
would fire. This was ad hoc, so remove it and always inline the value.

Consequently, the four func_pointer test functions that store a function
pointer into an array element (assign_from_agg, use_array_slot,
array_runtime_idx, multilayer) no longer verify: the inlined
of_fn_div (pre_of __fp) (post_of __fp) __fp value makes array_spec_upd s i v
too large for the array_spec_upd_* SMTPats to fire, so the read-back cannot
prove array_spec_mask/array_spec_initd nor recover the stored pointer.
Raising z3rlimit does not help (verified: fails identically at 50 and 300) --
it is a trigger/matching problem, not a resource-budget one. Comment those
functions out with an explanatory note until a library-level fix is done.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
@hei411
Fix outdated comments in emit.rs referencing removed pre/post defs
c14b924 
Several comments still referred to the generated `func_<g>_pre`/`func_<g>_post`
slprop definitions, which were removed when fnptr pre/post moved to the inlined
`pre_of`/`post_of` projectors (commit 74ed5e0). Update them to describe the
current design (inlined pre/post spliced into the `func_<g>__fp` wrapper):
- funcptr_module_name / collect_addr_taken / FnPtrSpecCore / FnRef / emit_of_fn
  doc comments.
- The `req ==> ens` rationale now references the inlined post slprop.
- Remove a dangling, mis-attached doc comment (a leftover from a removed fnptr
  param-map field) that was wrongly documenting `fnptr_diverged`.

Comment-only changes; no emitted output changes.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
@hei411
Fix outdated FnRef doc comment in ir/mod.rs
ac7ca76 
The `FnRef` variant doc still described the deep-model value as
`of_fn func_<name>_pre func_<name>_post func_<name>__fp`, referencing the
removed generated pre/post defs. Update to the current
`of_fn (pre_of func_<name>__fp) (post_of func_<name>__fp) func_<name>__fp`.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
@hei411
Drop _old threading for function-pointer pointer args
1aff923 
Function-pointer arguments are now always emitted as plain values. Pointer
arguments keep their default `pts_to` permission (via the general
`emit_type_slprop` lowering), but the initial-pointee value is no longer
threaded through the FuncPtr domain, so a callee's relational `_old(*p)`
contract can no longer be expressed across an indirect call.

emit.rs:
- emit_fnptr_arg_tuple emits one plain component per argument.
- fnptr_domain_with_old replaced by plain fnptr_domain.
- emit_fnptr_spec_core drops the old-value domain component, the
  subst/binder machinery, the FnptrPtrSubst activation, and the pinned
  old/cur pts_to block; pointer params fall through to the general path.
- Removed dead infra: FnptrPtrSubst, PtrValNames, ownership_ptr_pointee,
  the fnptr_ptr_subst field, set_fnptr_phase, and the guarded *p / _old(*p)
  resolution branches.

test/func_pointer: disable ptr_arg_cb (unsupported _old across a FuncPtr);
keep inc as a normal _old function (no longer address-taken).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: e8f4a381-e050-4a8b-88b6-7181b3a74435
@hei411
Cleanup
cc604e1
gebner
gebner reviewed Jul 28, 2026
View reviewed changes
Comment thread src/pass/emit.rs Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@gebner gebner gebner requested changes

Requested changes must be addressed to merge this pull request.

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@hei411 @gebner