[acl2/acl2] 6278e0: [x86] Improve the PE tools.

[Eric W. Smith]

Branch: refs/heads/testing-kestrel
Home: https://github.com/acl2/acl2
Commit: 6278e0403fc15e501b3d855e9750a44e97bd35fd
https://github.com/acl2/acl2/commit/6278e0403fc15e501b3d855e9750a44e97bd35fd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/x86/parsers/pe-tools.lisp

Log Message:
-----------
[x86] Improve the PE tools.

Add some checks, make return types more uniform, add and de-localize some rules.


Commit: 649a2e8de93efc53b8822f242a4a72ced1d6fdc0
https://github.com/acl2/acl2/commit/649a2e8de93efc53b8822f242a4a72ced1d6fdc0
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp

Log Message:
-----------
[x86] Improve assumptions.

Make more assumptions pseudo-terms, verify guards, add rules.


Commit: 59c3a656676c83e46af7174a8b77687054ad01e7
https://github.com/acl2/acl2/commit/59c3a656676c83e46af7174a8b77687054ad01e7
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/unroller.lisp

Log Message:
-----------
[axe/x86] Improve assumption handling.

Now more code can be in :logic mode.


Commit: 97055403890f755fd69c69fd6e12c383e1b51aae
https://github.com/acl2/acl2/commit/97055403890f755fd69c69fd6e12c383e1b51aae
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-01 (Mon, 01 Dec 2025)

Changed paths:
A books/kestrel/axe/x86/examples/abs/abs-elf64.lisp
A books/kestrel/axe/x86/examples/abs/abs.c
A books/kestrel/axe/x86/examples/abs/abs.elf64
A books/kestrel/axe/x86/examples/abs/acl2-customization.lsp
A books/kestrel/axe/x86/examples/abs/cert.acl2

Log Message:
-----------
Merge.


Commit: b8dae0344d1f2ebb404aadce5bb79ae5dadd483f
https://github.com/acl2/acl2/commit/b8dae0344d1f2ebb404aadce5bb79ae5dadd483f
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/simpadd0.lisp
M books/kestrel/c/transformation/variables-in-computation-states.lisp

Log Message:
-----------
Merge.


Commit: 28c3c601d0818b52f4becc3ba5e39754c9a49059
https://github.com/acl2/acl2/commit/28c3c601d0818b52f4becc3ba5e39754c9a49059
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/abs/abs-elf64.lisp

Log Message:
-----------
Merge.


Commit: a2b9468705a23291271c314eb58d2e1838950a90
https://github.com/acl2/acl2/commit/a2b9468705a23291271c314eb58d2e1838950a90
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/loop-lifter.lisp

Log Message:
-----------
[axe/x86] Slightly improve loop-lifter.


Commit: 4b46a10ed0c5ff34fd941d6d0da94100b9a57d06
https://github.com/acl2/acl2/commit/4b46a10ed0c5ff34fd941d6d0da94100b9a57d06
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Build in 2 rules.

Also tweak a rule-list (not yet used).


Commit: 33ac7ee1dc8af4039bbbd3e74a0b948a6c9baf12
https://github.com/acl2/acl2/commit/33ac7ee1dc8af4039bbbd3e74a0b948a6c9baf12
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Tweak rule-lists.


Commit: a1a7924a63e2352d0360c8fc967498e2388d3d04
https://github.com/acl2/acl2/commit/a1a7924a63e2352d0360c8fc967498e2388d3d04
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-02 (Tue, 02 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/rule-lists.lisp

Log Message:
-----------
[axe/x86] Improve rule-lists.

Simplify examples accordingly.


Commit: 89ff828a249d87bcc44c35ceafa02017e0aa7bcd
https://github.com/acl2/acl2/commit/89ff828a249d87bcc44c35ceafa02017e0aa7bcd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:
M acl2-fns.lisp
M axioms.lisp
M books/kestrel/c/syntax/abstract-syntax-symbols.lisp
M books/kestrel/c/syntax/formalized.lisp
M books/kestrel/c/syntax/langdef-mapping.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp
M books/kestrel/c/transformation/proof-generation.lisp
M books/kestrel/c/transformation/tests/simpadd0/dowhile.lisp
M books/kestrel/c/transformation/tests/simpadd0/gg.lisp
M books/kestrel/c/transformation/tests/simpadd0/if.lisp
M books/kestrel/c/transformation/tests/simpadd0/ifelse.lisp
M books/kestrel/c/transformation/tests/simpadd0/logand.lisp
M books/kestrel/c/transformation/tests/simpadd0/logor.lisp
M books/kestrel/c/transformation/tests/simpadd0/old/dowhile.c
M books/kestrel/c/transformation/tests/simpadd0/old/gg.c
M books/kestrel/c/transformation/tests/simpadd0/old/if.c
M books/kestrel/c/transformation/tests/simpadd0/old/ifelse.c
M books/kestrel/c/transformation/tests/simpadd0/old/logand.c
M books/kestrel/c/transformation/tests/simpadd0/old/logor.c
M books/kestrel/c/transformation/tests/simpadd0/old/ternary_int.c
M books/kestrel/c/transformation/tests/simpadd0/old/while.c
M books/kestrel/c/transformation/tests/simpadd0/ternary-int.lisp
M books/kestrel/c/transformation/tests/simpadd0/while.lisp
M books/system/doc/acl2-doc.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html

Log Message:
-----------
Merge.


Commit: f3fec20eedc3601c6a18e07edb844ee60021d4bd
https://github.com/acl2/acl2/commit/f3fec20eedc3601c6a18e07edb844ee60021d4bd
Author: Eric Smith <ews...@gmail.com>
Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp

Log Message:
-----------
[axe/x86] Reduce includes.


Compare: https://github.com/acl2/acl2/compare/9322aec2bc6f...f3fec20eedc3

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

[acl2buildserver]

Branch: refs/heads/master

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

Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp

M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp

M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp

M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp

M books/kestrel/x86/parsers/pe-tools.lisp

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

Merge commit 'f3fec20eedc3601c6a18e07edb844ee60021d4bd' into HEAD


Compare: https://github.com/acl2/acl2/compare/9fb9f75c893e...c2114a64b9b3

[acl2buildserver]

Branch: refs/heads/testing

[Alessandro Coglio]

Branch: refs/heads/testing-user-01

Commit: 3b407c134d1dde9bfcb4ba6331536dc2cf4fbf47
https://github.com/acl2/acl2/commit/3b407c134d1dde9bfcb4ba6331536dc2cf4fbf47
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/execution-limit-monotonicity.lisp

M books/kestrel/c/language/execution-without-function-calls.lisp
M books/kestrel/c/language/object-type-preservation.lisp
M books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/variable-resolution-preservation.lisp
M books/kestrel/c/language/variable-visibility-preservation.lisp

Log Message:
-----------
[C] Improve dynamic semantics.

Add and use `exec-expr-list`, mutually recursive with the other execution
functions. This eliminates the use of `exec-expr-pure-list` from those
functions.

Extend and adapt theorems about dynamic semantics.

Extend notion of limit for pure expression execution to lists of expressions,
and add theorems relating `exec-expr-list` to `exec-expr-pure-list`, similar to
the ones relating `exec-expr` and `exec-expr-pure`.


Commit: b9c47e9b23d68ecb6aa54f66cb589f4d417ef4db
https://github.com/acl2/acl2/commit/b9c47e9b23d68ecb6aa54f66cb589f4d417ef4db
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp

Log Message:
-----------
[ATC] Adapt to changes to dynamic semantics.


Commit: f7263b2cb69ebbf64d94115da30ea96e50c33b20
https://github.com/acl2/acl2/commit/f7263b2cb69ebbf64d94115da30ea96e50c33b20
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/axe/x86/examples/switch/support.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-1a-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64.lisp
M books/kestrel/axe/x86/examples/switch/switch-complex-elf64staticO2.lisp
M books/kestrel/axe/x86/examples/switch/switch-macho64.lisp
M books/kestrel/axe/x86/loop-lifter.lisp
M books/kestrel/axe/x86/rule-lists.lisp
M books/kestrel/axe/x86/unroller.lisp
M books/kestrel/x86/.sys/assump...@useless-runes.lsp
M books/kestrel/x86/assumptions-for-inputs.lisp
M books/kestrel/x86/assumptions.lisp
M books/kestrel/x86/assumptions32.lisp
M books/kestrel/x86/parsers/pe-tools.lisp

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

Merge.


Compare: https://github.com/acl2/acl2/compare/9fb9f75c893e...f7263b2cb69e

[Alessandro Coglio]

Branch: refs/heads/testing-acl2s

Commit: 9fb9f75c893e1a00edb61615ccd342dcb9f36277
https://github.com/acl2/acl2/commit/9fb9f75c893e1a00edb61615ccd342dcb9f36277
Author: Alessandro Coglio <em...@alessandrocoglio.info>

Date: 2025-12-03 (Wed, 03 Dec 2025)

Changed paths:

M books/kestrel/c/atc/tutorial.lisp

Log Message:
-----------
[ATC] Update some file references in the tutorial.

Thank you for Eric McCarthy for noticing the stale references.

Commit: 3da9e74b0a766269be27b1cfb383f46623eb29f7
https://github.com/acl2/acl2/commit/3da9e74b0a766269be27b1cfb383f46623eb29f7

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:
M books/kestrel/c/language/dynamic-semantics.lisp

Log Message:
-----------
[C] Update some doc.


Commit: f3a717c1a3e42181ea7a679665d6c98b3ddaf375
https://github.com/acl2/acl2/commit/f3a717c1a3e42181ea7a679665d6c98b3ddaf375

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:

M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/language/dynamic-semantics.lisp
M books/kestrel/c/language/pure-expression-execution.lisp

Log Message:
-----------
[C] Move some code.

Move `exec-expr-list` and `exec-expr-pure-list` away from the main file with the
dynamic semantics, because they are no longer part of the definition.


Commit: fd800b5c930847065d87e7cad0e0be451832cd9f
https://github.com/acl2/acl2/commit/fd800b5c930847065d87e7cad0e0be451832cd9f

Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2025-12-04 (Thu, 04 Dec 2025)

Changed paths:

A books/kestrel/c/atc/pure-expression-execution.lisp
M books/kestrel/c/atc/statement-generation.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-asg.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-call.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-expr-when-pure.lisp
M books/kestrel/c/atc/symbolic-execution-rules/exec-stmt.lisp
R books/kestrel/c/language/pure-expression-execution.lisp
M books/kestrel/c/language/top.lisp
M books/kestrel/c/transformation/proof-generation-theorems.lisp

Log Message:
-----------
[C] [ATC] [C2C] Move pure expression execution to ATC.

This is now only used by ATC; see added documentation.

We also eliminate a no-longer-needed book inclusion from C2C.


Compare: https://github.com/acl2/acl2/compare/9322aec2bc6f...fd800b5c9308