[acl2/acl2] 8019b0: [C2C] Support typedefs of the split struct type.

[Grant Jurgensen]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 8019b04aba05d401d4640b20803f809197c58d99
https://github.com/acl2/acl2/commit/8019b04aba05d401d4640b20803f809197c58d99
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/typedef-chain.c

Log Message:
-----------
[C2C] Support typedefs of the split struct type.

Now that the validator assigns unique identifiers to typedefs, a typedef
of a splittable type is split into a parallel right typedef, and uses of
the typedef name are substituted via the identifier map. Typedef
declarations reuse the existing uid-keyed declarator renaming, so the
core change is the type-spec typedef use case; the four rejection sites
and two detectors are removed. Add tests for direct, pointer, and chained
typedefs.


Commit: a5ad071b5e088b6ae757d0642ce1beaf18fdc31a
https://github.com/acl2/acl2/commit/a5ad071b5e088b6ae757d0642ce1beaf18fdc31a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Annotate member access expressions with their type

Add an info field to the :member and :memberp expression cases, and have
the validator store the access's result type there as a type-vinfo.


Commit: 2690383e7bda293cdd790ca7d74dbfad71fc245e
https://github.com/acl2/acl2/commit/2690383e7bda293cdd790ca7d74dbfad71fc245e
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------
[C2C] Preserve member access info in simpadd0 and subst-free

Carry the info field when rebuilding :member and :memberp nodes, now that
those expressions are annotated with their type.


Commit: 4686ea5663116acb216fce7aa9cde7f9f7b8964a
https://github.com/acl2/acl2/commit/4686ea5663116acb216fce7aa9cde7f9f7b8964a
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/split-gso.lisp

Log Message:
-----------
[C2C] Fix split-gso illegal GSO member access check

Preserve the info field when rebuilding member nodes. Fix the check for a
global struct object appearing in an address, sizeof, or alignof
expression: it cased the operand itself as an identifier rather than the
member access's sub-expression, so it never fired. Raise and return an
irrelevant expression in that case.


Commit: 6a7176b913a6eb3a41fb71bb2b5396c8d5926c1f
https://github.com/acl2/acl2/commit/6a7176b913a6eb3a41fb71bb2b5396c8d5926c1f
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/validation-annotations.lisp

Log Message:
-----------
[C$] Make expr-type precise for member access expressions

Return the annotated type of a :member or :memberp expression instead of
the unknown type, now that the validator records it.


Commit: 4da0f5629719acd73d489da80cb20d7647e60696
https://github.com/acl2/acl2/commit/4da0f5629719acd73d489da80cb20d7647e60696
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C2C] Rename the struct-uid state field to target-struct-uid

Clarify that this sts-split-state field is the unique identifier of the
struct type being split, distinguishing it from the struct type of a
member to be introduced later. The helper-function parameters keep the
struct-uid name.


Commit: afc44bf00b2cf5a09d5ea5b5401a455cc3e2a080
https://github.com/acl2/acl2/commit/afc44bf00b2cf5a09d5ea5b5401a455cc3e2a080
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[C2C] Support splitting a struct type that is a member of other structs

A member of splittable type is now split in place into two members: the
original on the left and a renamed copy of the right struct type. Member
accesses of splittable type are routed accordingly, and the renaming is
recorded in a new member-map of the state, keyed by the enclosing struct
type's unique identifier. The right member names are chosen
deterministically from each struct type's own member names, so that
compatible struct types remain compatible. Members of union types and
self-referential members remain unsupported. Initializers of objects
with split members are not yet supported.


Commit: 56ea4ec18165b9096c25b947c481358b72ce6c30
https://github.com/acl2/acl2/commit/56ea4ec18165b9096c25b947c481358b72ce6c30
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validator.lisp

Log Message:
-----------
[C$] Record initializer designations relative to the current brace

The validator recorded the implicit designation of a positional
initializer as the full path from the outermost object, which is not a
valid designation within a nested brace. Enter a fresh subobjects stack
rooted at the current object instead, so the designation is relative to
it. Add a validator test.


Commit: 34c3d49e094a706660d64bf05962190e1643b6ad
https://github.com/acl2/acl2/commit/34c3d49e094a706660d64bf05962190e1643b6ad
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/member-init.c
A books/kestrel/c/transformation/tests/struct-type-split/nested-init.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[C2C] Split initializers of members of splittable type

Extend the in-place splitting of members of splittable type to their
initializers, via a type-directed traversal of aggregate initializers.
By-value and pointer member initializers are now supported. Add tests.


Commit: a8c5891349ce05a0a55f7476abfb36c679353b24
https://github.com/acl2/acl2/commit/a8c5891349ce05a0a55f7476abfb36c679353b24
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp

Log Message:
-----------
[C2C] Document in-place splitting of members of splittable type

Document that members of splittable type in other struct types are
split in place, and the remaining exclusions (union members, anonymous
nesting, self-reference).


Commit: 97ac2323840c4b26ab9c6e948f86231b1da2d052
https://github.com/acl2/acl2/commit/97ac2323840c4b26ab9c6e948f86231b1da2d052
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/anon-struct.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/untagged-member.c
A books/kestrel/c/transformation/tests/struct-type-split/untagged-ptr.c

Log Message:
-----------
[C2C] Support splitting members of untagged struct types

Allow a directly splittable member of an untagged (e.g. typedef'd)
struct type to be split in place, like a member of a tagged struct
type. A splittable member reached only through an anonymous (promoted)
member remains unsupported.


Commit: fa019fe84a046a9a3dbc89c83eff5d9470b36414
https://github.com/acl2/acl2/commit/fa019fe84a046a9a3dbc89c83eff5d9470b36414
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/tests/struct-type-split/anon-struct.c
A books/kestrel/c/transformation/tests/struct-type-split/anon-union.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[C2C] Support splitting members of anonymous struct members

A directly splittable member of an anonymous struct member is split in
place and registered under the enclosing struct type, into which it is
promoted, so that its promoted accesses are routed. A member promoted
through an anonymous union member remains unsupported.


Commit: 588e820cb73cf46b1dfcfa05c96926f8a66e4c5b
https://github.com/acl2/acl2/commit/588e820cb73cf46b1dfcfa05c96926f8a66e4c5b
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp

Log Message:
-----------
[C2C] Document splitting members of untagged and anonymous struct types

Document that members of untagged struct types, and members promoted
from anonymous struct members, are split in place; members of unions,
including anonymous union members, remain excluded.


Commit: 82cb13607637a37ebeaeae6e400c780bdd0c0fba
https://github.com/acl2/acl2/commit/82cb13607637a37ebeaeae6e400c780bdd0c0fba
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/blacklist.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[C2C] Avoid right member name collisions with promoted members

Choose a fresh right member name that avoids the enclosing struct type's
full member namespace, including members promoted from anonymous members,
taken from the type completions.


Commit: 6bb992a84512782057acdfd22675243197ea6960
https://github.com/acl2/acl2/commit/6bb992a84512782057acdfd22675243197ea6960
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/fn-param-member.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

Log Message:
-----------
[C2C] Allow the split struct type within function parameter and return types

Check function parameter and return types like object types, so the split
struct type may occur as a member within them. Such an occurrence is split
in the member's struct type, leaving the parameter or return type unchanged.


Commit: 0ee184230306e4a9a72c1b77f29024b8d31942b6
https://github.com/acl2/acl2/commit/0ee184230306e4a9a72c1b77f29024b8d31942b6
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
[C2C] Replace maybe-msgp with msgp.


Commit: 1fd6ccc11dee0ca1641390353c706cc0332ebfcf
https://github.com/acl2/acl2/commit/1fd6ccc11dee0ca1641390353c706cc0332ebfcf
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp

Log Message:
-----------
Merge branch 'gj-struct-type-split' into testing-kestrel


Commit: 9086267d79137385effb2bec18c07cf8f83bcca3
https://github.com/acl2/acl2/commit/9086267d79137385effb2bec18c07cf8f83bcca3
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/top.acl2
A books/kestrel/c/transformation/json-rpc/.gitignore
A books/kestrel/c/transformation/json-rpc/README.md
A books/kestrel/c/transformation/json-rpc/acl2-customization.lsp
A books/kestrel/c/transformation/json-rpc/cert.acl2
A books/kestrel/c/transformation/json-rpc/save-exec-for-server.sh
A books/kestrel/c/transformation/json-rpc/server.sh
A books/kestrel/c/transformation/json-rpc/struct-type-split.lisp
A books/kestrel/c/transformation/json-rpc/tests/.gitignore
A books/kestrel/c/transformation/json-rpc/tests/cert.acl2
A books/kestrel/c/transformation/json-rpc/tests/example-request.json
A books/kestrel/c/transformation/json-rpc/tests/input-files/test1.c
A books/kestrel/c/transformation/json-rpc/tests/struct-type-split.lsp
A books/kestrel/c/transformation/json-rpc/tests/test-malformed-requests.sh
A books/kestrel/c/transformation/json-rpc/top.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/top.acl2
M books/kestrel/c/transformation/top.lisp

Log Message:
-----------
[C2C] Add a JSON-RPC interface to the C transformations.

This adds books/kestrel/c/transformation/json-rpc, a JSON-RPC 2.0 interface (built on the kestrel/jsonrpc library) that exposes the C-to-C transformations as JSON-RPC methods. The only method so far is struct-type-split, implemented as a guard-verified function in the JSONRPC package that drives the programmatic input-files, transformation, and output-files cores. The directory also provides a TCP socket server launcher and save-exec script, XDOC, a unit-test script, and an integration test for malformed requests. The interface is included from transformation/top, which requires the :jsonrpc-socket trust tag added here. A true-listp type-prescription on sts-split-code-ensemble's warnings is also added via more-returns.


Commit: 5eeaf8558ecd67709947f196b07c7cb0a129514f
https://github.com/acl2/acl2/commit/5eeaf8558ecd67709947f196b07c7cb0a129514f
Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/top.acl2
A books/kestrel/c/transformation/json-rpc/.gitignore
A books/kestrel/c/transformation/json-rpc/README.md
A books/kestrel/c/transformation/json-rpc/acl2-customization.lsp
A books/kestrel/c/transformation/json-rpc/cert.acl2
A books/kestrel/c/transformation/json-rpc/save-exec-for-server.sh
A books/kestrel/c/transformation/json-rpc/server.sh
A books/kestrel/c/transformation/json-rpc/struct-type-split.lisp
A books/kestrel/c/transformation/json-rpc/tests/.gitignore
A books/kestrel/c/transformation/json-rpc/tests/cert.acl2
A books/kestrel/c/transformation/json-rpc/tests/example-request.json
A books/kestrel/c/transformation/json-rpc/tests/input-files/test1.c
A books/kestrel/c/transformation/json-rpc/tests/struct-type-split.lsp
A books/kestrel/c/transformation/json-rpc/tests/test-malformed-requests.sh
A books/kestrel/c/transformation/json-rpc/top.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/top.acl2
M books/kestrel/c/transformation/top.lisp

Log Message:
-----------
Merge branch 'gj-json-rpc' into testing-kestrel


Compare: https://github.com/acl2/acl2/compare/3e3d172347f9...5eeaf8558ecd

To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications

[acl2buildserver]

Branch: refs/heads/master

Commit: 6f9addf19744cbabe65cf552b5a3ad3981a68e8c
https://github.com/acl2/acl2/commit/6f9addf19744cbabe65cf552b5a3ad3981a68e8c

Author: Grant Jurgensen <gr...@jurgensen.dev>
Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/top.acl2

M books/kestrel/c/transformation/struct-type-split.lisp
M books/kestrel/c/transformation/top.acl2

Log Message:
-----------
[C2C] Fix old symbol and ttags


Commit: fae82569b0831bd18db1052b4cfd12cc2440735a
https://github.com/acl2/acl2/commit/fae82569b0831bd18db1052b4cfd12cc2440735a
Author: ACL2 Build Server <acl2bui...@gmail.com>

Date: 2026-07-07 (Tue, 07 Jul 2026)

Changed paths:
M books/kestrel/c/syntax/abstract-syntax-trees.lisp

M books/kestrel/c/syntax/initializer-validation.lisp
M books/kestrel/c/syntax/tests/validator.lisp
M books/kestrel/c/syntax/validation-annotations.lisp
M books/kestrel/c/syntax/validator.lisp

M books/kestrel/c/top.acl2
A books/kestrel/c/transformation/json-rpc/.gitignore
A books/kestrel/c/transformation/json-rpc/README.md
A books/kestrel/c/transformation/json-rpc/acl2-customization.lsp
A books/kestrel/c/transformation/json-rpc/cert.acl2
A books/kestrel/c/transformation/json-rpc/save-exec-for-server.sh
A books/kestrel/c/transformation/json-rpc/server.sh
A books/kestrel/c/transformation/json-rpc/struct-type-split.lisp
A books/kestrel/c/transformation/json-rpc/tests/.gitignore
A books/kestrel/c/transformation/json-rpc/tests/cert.acl2
A books/kestrel/c/transformation/json-rpc/tests/example-request.json
A books/kestrel/c/transformation/json-rpc/tests/input-files/test1.c
A books/kestrel/c/transformation/json-rpc/tests/struct-type-split.lsp
A books/kestrel/c/transformation/json-rpc/tests/test-malformed-requests.sh
A books/kestrel/c/transformation/json-rpc/top.lisp

M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/split-gso.lisp
M books/kestrel/c/transformation/struct-type-split-doc.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
A books/kestrel/c/transformation/tests/struct-type-split/anon-struct.c
A books/kestrel/c/transformation/tests/struct-type-split/anon-union.c
A books/kestrel/c/transformation/tests/struct-type-split/blacklist.c
A books/kestrel/c/transformation/tests/struct-type-split/fn-param-member.c

A books/kestrel/c/transformation/tests/struct-type-split/member-init.c
A books/kestrel/c/transformation/tests/struct-type-split/nested-init.c
M books/kestrel/c/transformation/tests/struct-type-split/struct-type-split.lisp

A books/kestrel/c/transformation/tests/struct-type-split/untagged-member.c
A books/kestrel/c/transformation/tests/struct-type-split/untagged-ptr.c
A books/kestrel/c/transformation/top.acl2
M books/kestrel/c/transformation/top.lisp

M books/kestrel/c/transformation/utilities/subst-free.lisp

Log Message:
-----------

Merge commit '6f9addf19744cbabe65cf552b5a3ad3981a68e8c' into HEAD


Compare: https://github.com/acl2/acl2/compare/523a2e97d7bc...fae82569b083

[acl2buildserver]

Branch: refs/heads/testing