[acl2/acl2] 28e7d3: Fix CMPPS/CMPPD/CMPSS/CMPSD predicate imm8 mask
0 views
Skip to first unread message
Eric W. Smith
Jun 22, 2026, 7:39:49 PM (2 days ago) Jun 22
to acl2-...@googlegroups.com
Branch: refs/heads/x86-alt-defs
Home: https://github.com/acl2/acl2
Commit: 28e7d3307276f99967d75201c466f27165867655
https://github.com/acl2/acl2/commit/28e7d3307276f99967d75201c466f27165867655
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/logical.lisp
Log Message:
-----------
Fix CMPPS/CMPPD/CMPSS/CMPSD predicate imm8 mask
The CMPPS, CMPPD, CMPSS, and CMPSD instructions use the low 3 bits of
imm8 as a comparison predicate. Bits 3-7 are reserved per the Intel SDM.
The model was reading only the low 2 bits via (n02 imm), so predicates
4-7 (NEQ, NLT, NLE, ORD) collapsed to 0-3 (EQ, LT, LE, UNORD), producing
the inverse of the correct comparison result.
Change (n02 imm) to (n03 imm) in the four predicate-reading locations in
fp/logical.lisp so that bits 2:0 are used as the predicate selector.
Verified by make test in tools/execution/asmtest:
testgen_1332 (CMPPS): 0 mismatches
testgen_1345 (CMPSS): 0 mismatches
testgen_1347 (CMPPD): 0 mismatches
testgen_1351 (CMPSD): 0 mismatches
Commit: 1b905154b1a3f3d3b0edfa7477f62515b7919c9b
https://github.com/acl2/acl2/commit/1b905154b1a3f3d3b0edfa7477f62515b7919c9b
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
Fix PSLLDQ/PSRLDQ count>=16 to zero the destination
Per the Intel SDM, if the count operand to PSLLDQ/PSRLDQ is greater than
15, the destination operand is set to all zeros. The SDM pseudocode
sets TEMP := 16 in this case so that the subsequent 128-bit shift
produces zero. The model instead clamped count to 0, making the
instruction a no-op rather than zeroing.
Change the clamp to 16 instead of 0 so the shift produces the
required zero result.
Verified by make test in tools/execution/asmtest:
testgen_666 (PSRLDQ): 0 mismatches
testgen_667 (PSLLDQ): 0 mismatches
Commit: b1d82e368cf64b18f4a7e4c24808ce37d96c8b82
https://github.com/acl2/acl2/commit/b1d82e368cf64b18f4a7e4c24808ce37d96c8b82
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/bit.lisp
Log Message:
-----------
Fix LZCNT helper to start search at MSB
The recursive lzcnt helper counts leading zeros by walking bits from the
MSB downward. Its base case fires when the index (i+1) reaches 0, and
its only call site passed an initial i+1 of 0, so the helper returned
the operand-size-bits value immediately for every input.
Change the initial i+1 to (ash operand-size 3) (= bits) so the first
iteration examines bit (bits - 1), the MSB, and decrements toward 0.
Verified by make test in tools/execution/asmtest:
testgen_2025 (LZCNT): 0 mismatches
Commit: 2c797caa7970f2fec27fcb0f657f41fc5e35ecde
https://github.com/acl2/acl2/commit/2c797caa7970f2fec27fcb0f657f41fc5e35ecde
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
Log Message:
-----------
Fix VPOR VEX dispatch operation code
The VEX-encoded VPOR dispatch entries passed the XOR opcode constant instead of the OR opcode constant, causing the model to compute XMM9 ^ XMM10 (XOR) rather than XMM9 | XMM10 (OR) for every VPOR invocation.
Change the two (operation . #x5) entries to (operation . #.*OP-OR*) in inst-listing.lisp so that VEX-encoded VPOR performs a bitwise OR, using the symbolic constant used elsewhere in the instruction table.
Verified by make test in tools/execution/asmtest:
testgen_2555 (VPOR): 0 mismatches
Commit: 4bb7ddb6d91cb870b58eab4badfb5a145d693dcf
https://github.com/acl2/acl2/commit/4bb7ddb6d91cb870b58eab4badfb5a145d693dcf
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Preserve flags in shifts/rotates when count is zero
Per the Intel SDM, when the shift count is 0 no flags are affected for
SAL/SHL/SAR/SHR (sal:sar:shl:shr:551), SHLD/SHRD (shld:119, shrd:119),
and RCL/RCR/ROL/ROR (rcl:rcr:rol:ror:584). The spec functions in
shifts-spec.lisp and rotates-spec.lisp already handled the count=0
case for most instructions, but ROL/ROR marked OF as undefined for
src=0, contradicting the SDM ("For ROL and ROR instructions, if the
masked count is 0, the flags are not affected").
This commit:
1. Fixes rol-spec-gen and ror-spec-gen so their (src=0) branch
returns (mv input-rflags 0) instead of marking OF as undefined.
2. Removes the count=0 short-circuit at the dispatch sites in
x86-sal/sar/shl/shr/rcl/rcr/rol/ror and x86-shld/shrd. The
flag-preservation logic now lives entirely in the spec functions
(where the comment on each function notes the count=0 case), per
the review feedback that the dispatch site should not duplicate
flag computation.
The result of removing the short-circuit is functionally identical to
the prior behavior for SAL/SHL/SAR/SHR/RCL/RCR/SHLD/SHRD (whose spec
functions already returned (mv input-rflags 0) for count=0) and a
behavior fix for ROL/ROR.
Verified by make test in tools/execution/asmtest (after cert.pl on
top and asmtest):
ROL/ROR (no specific count=0 tests, but full-suite ROL/ROR
snippets report 0 mismatches):
testgen_365 (ROL r8b, imm8): 0
testgen_367 (ROL r64, imm8): 0
testgen_377 (ROR r8b, imm8): 0
testgen_378 (ROR r64, imm8): 0
testgen_397 (ROR r8b, CL): 0
testgen_399 (ROR r64, CL): 0
Sal/shl/sar/shr/shld/shrd (count=0 cascade mismatches from prior
instructions in the loop remain, per the PR description):
testgen_429 (SHL r8b): count=0 mismatches eliminated
testgen_433 (SHL r64): 0
testgen_435 (SHL r32): 0
testgen_445 (SHR r8b): count=0 mismatches eliminated
testgen_447 (SHR r32): 0
testgen_457 (SAR r8b): count=0 mismatches eliminated
testgen_459 (SAR r64): 0
testgen_1642 (SHRD): 0
testgen_1646 (SHLD): 0
Other PR fixes still pass:
testgen_1332 (CMPPS): 0
testgen_1345 (CMPSS): 0
testgen_1347 (CMPPD): 0
testgen_1351 (CMPSD): 0
testgen_666 (PSRLDQ): 0
testgen_667 (PSLLDQ): 0
testgen_2025 (LZCNT): 0
testgen_2555 (VPOR): 0
Commit: 83364f080d57e82054a4327dd8832e3083733600
https://github.com/acl2/acl2/commit/83364f080d57e82054a4327dd8832e3083733600
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
Log Message:
-----------
[x86] Fix alt-def proof.
Compare: https://github.com/acl2/acl2/compare/28e7d3307276%5E...83364f080d57
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Home: https://github.com/acl2/acl2
Commit: 28e7d3307276f99967d75201c466f27165867655
https://github.com/acl2/acl2/commit/28e7d3307276f99967d75201c466f27165867655
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/fp/logical.lisp
Log Message:
-----------
Fix CMPPS/CMPPD/CMPSS/CMPSD predicate imm8 mask
The CMPPS, CMPPD, CMPSS, and CMPSD instructions use the low 3 bits of
imm8 as a comparison predicate. Bits 3-7 are reserved per the Intel SDM.
The model was reading only the low 2 bits via (n02 imm), so predicates
4-7 (NEQ, NLT, NLE, ORD) collapsed to 0-3 (EQ, LT, LE, UNORD), producing
the inverse of the correct comparison result.
Change (n02 imm) to (n03 imm) in the four predicate-reading locations in
fp/logical.lisp so that bits 2:0 are used as the predicate selector.
Verified by make test in tools/execution/asmtest:
testgen_1332 (CMPPS): 0 mismatches
testgen_1345 (CMPSS): 0 mismatches
testgen_1347 (CMPPD): 0 mismatches
testgen_1351 (CMPSD): 0 mismatches
Commit: 1b905154b1a3f3d3b0edfa7477f62515b7919c9b
https://github.com/acl2/acl2/commit/1b905154b1a3f3d3b0edfa7477f62515b7919c9b
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/pshift.lisp
Log Message:
-----------
Fix PSLLDQ/PSRLDQ count>=16 to zero the destination
Per the Intel SDM, if the count operand to PSLLDQ/PSRLDQ is greater than
15, the destination operand is set to all zeros. The SDM pseudocode
sets TEMP := 16 in this case so that the subsequent 128-bit shift
produces zero. The model instead clamped count to 0, making the
instruction a no-op rather than zeroing.
Change the clamp to 16 instead of 0 so the shift produces the
required zero result.
Verified by make test in tools/execution/asmtest:
testgen_666 (PSRLDQ): 0 mismatches
testgen_667 (PSLLDQ): 0 mismatches
Commit: b1d82e368cf64b18f4a7e4c24808ce37d96c8b82
https://github.com/acl2/acl2/commit/b1d82e368cf64b18f4a7e4c24808ce37d96c8b82
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-20 (Sat, 20 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/bit.lisp
Log Message:
-----------
Fix LZCNT helper to start search at MSB
The recursive lzcnt helper counts leading zeros by walking bits from the
MSB downward. Its base case fires when the index (i+1) reaches 0, and
its only call site passed an initial i+1 of 0, so the helper returned
the operand-size-bits value immediately for every input.
Change the initial i+1 to (ash operand-size 3) (= bits) so the first
iteration examines bit (bits - 1), the MSB, and decrements toward 0.
Verified by make test in tools/execution/asmtest:
testgen_2025 (LZCNT): 0 mismatches
Commit: 2c797caa7970f2fec27fcb0f657f41fc5e35ecde
https://github.com/acl2/acl2/commit/2c797caa7970f2fec27fcb0f657f41fc5e35ecde
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/inst-listing.lisp
Log Message:
-----------
Fix VPOR VEX dispatch operation code
The VEX-encoded VPOR dispatch entries passed the XOR opcode constant instead of the OR opcode constant, causing the model to compute XMM9 ^ XMM10 (XOR) rather than XMM9 | XMM10 (OR) for every VPOR invocation.
Change the two (operation . #x5) entries to (operation . #.*OP-OR*) in inst-listing.lisp so that VEX-encoded VPOR performs a bitwise OR, using the symbolic constant used elsewhere in the instruction table.
Verified by make test in tools/execution/asmtest:
testgen_2555 (VPOR): 0 mismatches
Commit: 4bb7ddb6d91cb870b58eab4badfb5a145d693dcf
https://github.com/acl2/acl2/commit/4bb7ddb6d91cb870b58eab4badfb5a145d693dcf
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Preserve flags in shifts/rotates when count is zero
Per the Intel SDM, when the shift count is 0 no flags are affected for
SAL/SHL/SAR/SHR (sal:sar:shl:shr:551), SHLD/SHRD (shld:119, shrd:119),
and RCL/RCR/ROL/ROR (rcl:rcr:rol:ror:584). The spec functions in
shifts-spec.lisp and rotates-spec.lisp already handled the count=0
case for most instructions, but ROL/ROR marked OF as undefined for
src=0, contradicting the SDM ("For ROL and ROR instructions, if the
masked count is 0, the flags are not affected").
This commit:
1. Fixes rol-spec-gen and ror-spec-gen so their (src=0) branch
returns (mv input-rflags 0) instead of marking OF as undefined.
2. Removes the count=0 short-circuit at the dispatch sites in
x86-sal/sar/shl/shr/rcl/rcr/rol/ror and x86-shld/shrd. The
flag-preservation logic now lives entirely in the spec functions
(where the comment on each function notes the count=0 case), per
the review feedback that the dispatch site should not duplicate
flag computation.
The result of removing the short-circuit is functionally identical to
the prior behavior for SAL/SHL/SAR/SHR/RCL/RCR/SHLD/SHRD (whose spec
functions already returned (mv input-rflags 0) for count=0) and a
behavior fix for ROL/ROR.
Verified by make test in tools/execution/asmtest (after cert.pl on
top and asmtest):
ROL/ROR (no specific count=0 tests, but full-suite ROL/ROR
snippets report 0 mismatches):
testgen_365 (ROL r8b, imm8): 0
testgen_367 (ROL r64, imm8): 0
testgen_377 (ROR r8b, imm8): 0
testgen_378 (ROR r64, imm8): 0
testgen_397 (ROR r8b, CL): 0
testgen_399 (ROR r64, CL): 0
Sal/shl/sar/shr/shld/shrd (count=0 cascade mismatches from prior
instructions in the loop remain, per the PR description):
testgen_429 (SHL r8b): count=0 mismatches eliminated
testgen_433 (SHL r64): 0
testgen_435 (SHL r32): 0
testgen_445 (SHR r8b): count=0 mismatches eliminated
testgen_447 (SHR r32): 0
testgen_457 (SAR r8b): count=0 mismatches eliminated
testgen_459 (SAR r64): 0
testgen_1642 (SHRD): 0
testgen_1646 (SHLD): 0
Other PR fixes still pass:
testgen_1332 (CMPPS): 0
testgen_1345 (CMPSS): 0
testgen_1347 (CMPPD): 0
testgen_1351 (CMPSD): 0
testgen_666 (PSRLDQ): 0
testgen_667 (PSLLDQ): 0
testgen_2025 (LZCNT): 0
testgen_2555 (VPOR): 0
Commit: 83364f080d57e82054a4327dd8832e3083733600
https://github.com/acl2/acl2/commit/83364f080d57e82054a4327dd8832e3083733600
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-22 (Mon, 22 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
Log Message:
-----------
[x86] Fix alt-def proof.
Compare: https://github.com/acl2/acl2/compare/28e7d3307276%5E...83364f080d57
To unsubscribe from these emails, change your notification settings at https://github.com/acl2/acl2/settings/notifications
Yahya Sohail
Jun 23, 2026, 7:36:42 PM (5 hours ago) Jun 23
to acl2-...@googlegroups.com
Branch: refs/heads/testing
Commit: 39e12b30477263ef223237e744f7c3a994502e3d
https://github.com/acl2/acl2/commit/39e12b30477263ef223237e744f7c3a994502e3d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
Log Message:
-----------
[x86] Fix alt-def proof.
Commit: fb3eed579f18a362f6c9f4f26e92f0f414bd2edf
https://github.com/acl2/acl2/commit/fb3eed579f18a362f6c9f4f26e92f0f414bd2edf
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
x86isa: Fix 5 real model bugs in asmtest (CMPPS/PD/SS/SD, shifts, PSLLDQ/PSRLDQ, LZCNT, VPOR)
Compare: https://github.com/acl2/acl2/compare/ffa75ee4b479...fb3eed579f18
https://github.com/acl2/acl2/commit/39e12b30477263ef223237e744f7c3a994502e3d
Author: Eric Smith <ews...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
Log Message:
-----------
[x86] Fix alt-def proof.
https://github.com/acl2/acl2/commit/fb3eed579f18a362f6c9f4f26e92f0f414bd2edf
Author: Yahya Sohail <ya...@yahyasohail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/x86/alt-defs.lisp
M books/projects/x86isa/machine/inst-listing.lisp
M books/projects/x86isa/machine/instructions/bit.lisp
M books/projects/x86isa/machine/instructions/fp/logical.lisp
M books/projects/x86isa/machine/instructions/pshift.lisp
M books/projects/x86isa/machine/instructions/rotate-and-shift.lisp
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
Merge pull request #1957 from yaso9/x86isa-testgen-bug-fixes
M books/projects/x86isa/machine/instructions/rotates-spec.lisp
Log Message:
-----------
x86isa: Fix 5 real model bugs in asmtest (CMPPS/PD/SS/SD, shifts, PSLLDQ/PSRLDQ, LZCNT, VPOR)
Compare: https://github.com/acl2/acl2/compare/ffa75ee4b479...fb3eed579f18
acl2buildserver
Jun 23, 2026, 10:41:42 PM (2 hours ago) Jun 23
to acl2-...@googlegroups.com
Branch: refs/heads/master
Commit: 703070e6f1dfbbb62de0f8d7d2d4b326f422c264
https://github.com/acl2/acl2/commit/703070e6f1dfbbb62de0f8d7d2d4b326f422c264
Author: ACL2 Build Server <acl2bui...@gmail.com>
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
Merge commit '84da6ce4be738014f8973db71a203faa888f107d' into HEAD
Commit: 243dfab47d8aad22cee7176740da319cfbf6862f
https://github.com/acl2/acl2/commit/243dfab47d8aad22cee7176740da319cfbf6862f
Author: ACL2 Build Server <acl2bui...@gmail.com>
Log Message:
-----------
Merge commit '996e5aeb4b77122645622e529b8df624eee1ce21' into HEAD
Compare: https://github.com/acl2/acl2/compare/996e5aeb4b77...243dfab47d8a
https://github.com/acl2/acl2/commit/703070e6f1dfbbb62de0f8d7d2d4b326f422c264
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/c/syntax/null-pointer-constants.lisp
Changed paths:
M books/kestrel/c/syntax/types-formal-subset-and-mapping.lisp
M books/kestrel/c/syntax/types.lisp
M books/kestrel/c/syntax/validator.lisp
M books/kestrel/c/transformation/struct-type-split-safety.lisp
M books/kestrel/c/transformation/struct-type-split.lisp
Log Message:
-----------
Merge commit '84da6ce4be738014f8973db71a203faa888f107d' into HEAD
Commit: 243dfab47d8aad22cee7176740da319cfbf6862f
https://github.com/acl2/acl2/commit/243dfab47d8aad22cee7176740da319cfbf6862f
Author: ACL2 Build Server <acl2bui...@gmail.com>
Date: 2026-06-23 (Tue, 23 Jun 2026)
Changed paths:
M books/kestrel/remora/abstract-syntax-well-formed.lisp
Changed paths:
Log Message:
-----------
Merge commit '996e5aeb4b77122645622e529b8df624eee1ce21' into HEAD
Compare: https://github.com/acl2/acl2/compare/996e5aeb4b77...243dfab47d8a
Reply all
Reply to author
Forward
0 new messages