[acl2/acl2] 68f54d: [X86ISA] Add a stack address size selection operat...

[Alessandro Coglio]

Branch: refs/heads/master
Home: https://github.com/acl2/acl2
Commit: 68f54d6e2ffca319b51b4c3144ae5a5e089ad881
https://github.com/acl2/acl2/commit/68f54d6e2ffca319b51b4c3144ae5a5e089ad881
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/projects/x86isa/machine/decoding-and-spec-utils.lisp

Log Message:
-----------
[X86ISA] Add a stack address size selection operation.


Commit: afe43e81009e4af2449f3b41a49f4dd65489a9d9
https://github.com/acl2/acl2/commit/afe43e81009e4af2449f3b41a49f4dd65489a9d9
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/subroutine.lisp

Log Message:
-----------
[X86ISA] Use stack address size in LEAVE.

Remove an unwarranted simplification according to which we were using the
operand size in a part of the code instead of the stack address size. The two
sizes are normally the same, but we want to model the exact behavior of the
instruction.


Commit: 2a72af7674bc3f1ff6e30b152ee54411bc27d965
https://github.com/acl2/acl2/commit/2a72af7674bc3f1ff6e30b152ee54411bc27d965
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/subroutine.lisp

Log Message:
-----------
[X86ISA] Use stack address size in ENTER.

This is similar to the fix done to LEAVE. Although the stack address size is
normally the same as the operand size, this is not precise w.r.t. the Intel
manual.


Commit: 0e5e3b48668b073b1175f4c728cd9cabafe25d91
https://github.com/acl2/acl2/commit/0e5e3b48668b073b1175f4c728cd9cabafe25d91
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/kestrel/remora/dynamic-environments.lisp
M books/kestrel/remora/evaluation.lisp
A books/kestrel/remora/primitives-evaluation-length-tests.lisp
M books/kestrel/remora/primitives-evaluation.lisp
M books/kestrel/remora/static-environments.lisp
M books/kestrel/remora/values.lisp

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


Commit: 5a87eacedd1f59cc76d08df793c3e6227960e470
https://github.com/acl2/acl2/commit/5a87eacedd1f59cc76d08df793c3e6227960e470
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-03 (Fri, 03 Jul 2026)

Changed paths:
M books/projects/x86isa/machine/instructions/subroutine.lisp

Log Message:
-----------
[X86ISA] Add some doc.


Commit: d507342ae23b59a909383f6ab24050db45dbb2a8
https://github.com/acl2/acl2/commit/d507342ae23b59a909383f6ab24050db45dbb2a8
Author: Alessandro Coglio <em...@alessandrocoglio.info>
Date: 2026-07-04 (Sat, 04 Jul 2026)

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

Log Message:
-----------
[Axe x86] Add rule for newly added function.


Compare: https://github.com/acl2/acl2/compare/737e0f7a9008...d507342ae23b

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

[Alessandro Coglio]

Branch: refs/heads/testing