-
Notifications
You must be signed in to change notification settings - Fork 147
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Add some assembly tests from BoringSSL p256
Towards better equivalence checking
We don't support these instructions yet:
```
$ src/ExtractionOCaml/word_by_word_montgomery p256 64 '2^256 - 2^224 + 2^192 + 2^96 - 1' mul --no-wide-int --shiftr-avoid-uint1 --hints-file fiat-amd64/boringssl_intel_manual_mul_p256.asm
[...]
In parsing:
Error while parsing assembly:
mul r9
mul r10
mul r11
mul r12
mul r15
mov rax,QWORD PTR [rbx+0x8]
mul QWORD PTR [rsi]
mul QWORD PTR [rsi+0x8]
mul QWORD PTR [rsi+0x10]
mul QWORD PTR [rsi+0x18]
mul r15
mov rax,QWORD PTR [rbx+0x10]
mul QWORD PTR [rsi]
mul QWORD PTR [rsi+0x8]
mul QWORD PTR [rsi+0x10]
mul QWORD PTR [rsi+0x18]
mul r15
mov rax,QWORD PTR [rbx+0x18]
mul QWORD PTR [rsi]
mul QWORD PTR [rsi+0x8]
mul QWORD PTR [rsi+0x10]
mul QWORD PTR [rsi+0x18]
mul r15
cmovb r12,rcx
cmovb r13,rbp
mov QWORD PTR [rdi],r12
cmovb r8,rbx
mov QWORD PTR [rdi+0x8],r13
cmovb r9,rdx
mov QWORD PTR [rdi+0x10],r8
mov QWORD PTR [rdi+0x18],r9
repz ret
Fatal error: exception Failure("Synthesis failed")
```- Loading branch information
1 parent
56a01f2
commit 6882c07
Showing
4 changed files
with
853 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,165 @@ | ||
| __ecp_nistz256_mul_montq: | ||
| mov rbp,rax | ||
| mul r9 | ||
| mov r14,0x00000000ffffffff | ||
| mov r8,rax | ||
| mov rax,rbp | ||
| mov r9,rdx | ||
| mul r10 | ||
| mov r15,0xffffffff00000001 | ||
| add r9,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov r10,rdx | ||
| mul r11 | ||
| add r10,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov r11,rdx | ||
| mul r12 | ||
| add r11,rax | ||
| mov rax,r8 | ||
| adc rdx,0x0 | ||
| xor r13,r13 | ||
| mov r12,rdx | ||
| mov rbp,r8 | ||
| shl r8,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r9,r8 | ||
| adc r10,rbp | ||
| adc r11,rax | ||
| mov rax,QWORD PTR [rbx+0x8] | ||
| adc r12,rdx | ||
| adc r13,0x0 | ||
| xor r8,r8 | ||
| mov rbp,rax | ||
| mul QWORD PTR [rsi] | ||
| add r9,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x8] | ||
| add r10,rcx | ||
| adc rdx,0x0 | ||
| add r10,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x10] | ||
| add r11,rcx | ||
| adc rdx,0x0 | ||
| add r11,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x18] | ||
| add r12,rcx | ||
| adc rdx,0x0 | ||
| add r12,rax | ||
| mov rax,r9 | ||
| adc r13,rdx | ||
| adc r8,0x0 | ||
| mov rbp,r9 | ||
| shl r9,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r10,r9 | ||
| adc r11,rbp | ||
| adc r12,rax | ||
| mov rax,QWORD PTR [rbx+0x10] | ||
| adc r13,rdx | ||
| adc r8,0x0 | ||
| xor r9,r9 | ||
| mov rbp,rax | ||
| mul QWORD PTR [rsi] | ||
| add r10,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x8] | ||
| add r11,rcx | ||
| adc rdx,0x0 | ||
| add r11,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x10] | ||
| add r12,rcx | ||
| adc rdx,0x0 | ||
| add r12,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x18] | ||
| add r13,rcx | ||
| adc rdx,0x0 | ||
| add r13,rax | ||
| mov rax,r10 | ||
| adc r8,rdx | ||
| adc r9,0x0 | ||
| mov rbp,r10 | ||
| shl r10,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r11,r10 | ||
| adc r12,rbp | ||
| adc r13,rax | ||
| mov rax,QWORD PTR [rbx+0x18] | ||
| adc r8,rdx | ||
| adc r9,0x0 | ||
| xor r10,r10 | ||
| mov rbp,rax | ||
| mul QWORD PTR [rsi] | ||
| add r11,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x8] | ||
| add r12,rcx | ||
| adc rdx,0x0 | ||
| add r12,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x10] | ||
| add r13,rcx | ||
| adc rdx,0x0 | ||
| add r13,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x18] | ||
| add r8,rcx | ||
| adc rdx,0x0 | ||
| add r8,rax | ||
| mov rax,r11 | ||
| adc r9,rdx | ||
| adc r10,0x0 | ||
| mov rbp,r11 | ||
| shl r11,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r12,r11 | ||
| adc r13,rbp | ||
| mov rcx,r12 | ||
| adc r8,rax | ||
| adc r9,rdx | ||
| mov rbp,r13 | ||
| adc r10,0x0 | ||
| sub r12,0xffffffffffffffff | ||
| mov rbx,r8 | ||
| sbb r13,r14 | ||
| sbb r8,0x0 | ||
| mov rdx,r9 | ||
| sbb r9,r15 | ||
| sbb r10,0x0 | ||
| cmovb r12,rcx | ||
| cmovb r13,rbp | ||
| mov QWORD PTR [rdi],r12 | ||
| cmovb r8,rbx | ||
| mov QWORD PTR [rdi+0x8],r13 | ||
| cmovb r9,rdx | ||
| mov QWORD PTR [rdi+0x10],r8 | ||
| mov QWORD PTR [rdi+0x18],r9 | ||
| repz ret |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,165 @@ | ||
| __ecp_nistz256_mul_montq: | ||
| mov rbp,rax | ||
| mul r9 | ||
| mov r14,0x00000000ffffffff | ||
| mov r8,rax | ||
| mov rax,rbp | ||
| mov r9,rdx | ||
| mul r10 | ||
| mov r15,0xffffffff00000001 | ||
| add r9,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov r10,rdx | ||
| mul r11 | ||
| add r10,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov r11,rdx | ||
| mul r12 | ||
| add r11,rax | ||
| mov rax,r8 | ||
| adc rdx,0x0 | ||
| xor r13,r13 | ||
| mov r12,rdx | ||
| mov rbp,r8 | ||
| shl r8,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r9,r8 | ||
| adc r10,rbp | ||
| adc r11,rax | ||
| mov rax,QWORD PTR [rbx+0x8] | ||
| adc r12,rdx | ||
| adc r13,0x0 | ||
| xor r8,r8 | ||
| mov rbp,rax | ||
| mul QWORD PTR [rsi] | ||
| add r9,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x8] | ||
| add r10,rcx | ||
| adc rdx,0x0 | ||
| add r10,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x10] | ||
| add r11,rcx | ||
| adc rdx,0x0 | ||
| add r11,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x18] | ||
| add r12,rcx | ||
| adc rdx,0x0 | ||
| add r12,rax | ||
| mov rax,r9 | ||
| adc r13,rdx | ||
| adc r8,0x0 | ||
| mov rbp,r9 | ||
| shl r9,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r10,r9 | ||
| adc r11,rbp | ||
| adc r12,rax | ||
| mov rax,QWORD PTR [rbx+0x10] | ||
| adc r13,rdx | ||
| adc r8,0x0 | ||
| xor r9,r9 | ||
| mov rbp,rax | ||
| mul QWORD PTR [rsi] | ||
| add r10,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x8] | ||
| add r11,rcx | ||
| adc rdx,0x0 | ||
| add r11,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x10] | ||
| add r12,rcx | ||
| adc rdx,0x0 | ||
| add r12,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x18] | ||
| add r13,rcx | ||
| adc rdx,0x0 | ||
| add r13,rax | ||
| mov rax,r10 | ||
| adc r8,rdx | ||
| adc r9,0x0 | ||
| mov rbp,r10 | ||
| shl r10,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r11,r10 | ||
| adc r12,rbp | ||
| adc r13,rax | ||
| mov rax,QWORD PTR [rbx+0x18] | ||
| adc r8,rdx | ||
| adc r9,0x0 | ||
| xor r10,r10 | ||
| mov rbp,rax | ||
| mul QWORD PTR [rsi] | ||
| add r11,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x8] | ||
| add r12,rcx | ||
| adc rdx,0x0 | ||
| add r12,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x10] | ||
| add r13,rcx | ||
| adc rdx,0x0 | ||
| add r13,rax | ||
| mov rax,rbp | ||
| adc rdx,0x0 | ||
| mov rcx,rdx | ||
| mul QWORD PTR [rsi+0x18] | ||
| add r8,rcx | ||
| adc rdx,0x0 | ||
| add r8,rax | ||
| mov rax,r11 | ||
| adc r9,rdx | ||
| adc r10,0x0 | ||
| mov rbp,r11 | ||
| shl r11,0x20 | ||
| mul r15 | ||
| shr rbp,0x20 | ||
| add r12,r11 | ||
| adc r13,rbp | ||
| mov rcx,r12 | ||
| adc r8,rax | ||
| adc r9,rdx | ||
| mov rbp,r13 | ||
| adc r10,0x0 | ||
| sub r12,0xffffffffffffffff | ||
| mov rbx,r8 | ||
| sbb r13,r14 | ||
| sbb r8,0x0 | ||
| mov rdx,r9 | ||
| sbb r9,r15 | ||
| sbb r10,0x0 | ||
| cmovb r12,rcx | ||
| cmovb r13,rbp | ||
| mov QWORD PTR [rdi],r12 | ||
| cmovb r8,rbx | ||
| mov QWORD PTR [rdi+0x8],r13 | ||
| cmovb r9,rdx | ||
| mov QWORD PTR [rdi+0x10],r8 | ||
| mov QWORD PTR [rdi+0x18],r9 | ||
| repz ret |
Oops, something went wrong.