Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error: tried to spill OF, but didnt work. TSNH. #204

Open
andres-erbsen opened this issue Sep 11, 2023 · 6 comments
Open

Error: tried to spill OF, but didnt work. TSNH. #204

andres-erbsen opened this issue Sep 11, 2023 · 6 comments

Comments

@andres-erbsen
Copy link

p256sqr2.zip

./CryptOpt --bridge manual --cFile ./p256sqr2.c --jsonFile ./p256sqr2.json --seed 2
Start on brg/symbolname>>manual/p256_sqr<< >>without proofing correct<< on cpu >>Intel(R) Xeon(R) CPU @ 2.80GHz<< writing results to>>/home/andreser/CryptOpt/results<< with seed >>4156876406132912<< for >>  200<< evaluations against CC>>gcc -march=native -mtune=native -O3<< with cycle goal>>10000<< for each measurement on host>>andreser<< with pid>>3079059<< using counter>>RDTSCP<< framePointer=>>omit<< memoryConstraints>>none<< starting @>>2023-09-11T19:23:01.677Z<<
{
  curOperation: {
    datatype: 'u64',
    name: [ 'x59', '_' ],
    operation: 'addcarryx',
    arguments: [ 'x58', 'x38', 'x40' ],
    decisions: {
      di_choose_arg: [Array],
      di_spill_location: [Array],
      di_flag: [Array],
      di_handle_flags_kk: [Array],
      di_choose_imm: [Array]
    },
    decisionsHot: []
  },
  e: Error: tried to spill OF, but didnt work. TSNH.
      at Jt (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:24964)
      at pe (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:37026)
      at $e (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:33719)
      at Ae (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:51131)
      at file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:61683
      at Timeout._onTimeout (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:62312)
      at listOnTimeout (node:internal/timers:573:17)
      at process.processTimers (node:internal/timers:514:7),
  allocs: {
    '0x100000000': { datatype: 'u64', store: 'r10' },
    arg1: { datatype: 'u64[4]', store: 'rsi' },
    'calSv-r12': { datatype: 'u64', store: '[ rsp - 0x70 ]' },
    'calSv-r13': { datatype: 'u64', store: '[ rsp - 0x68 ]' },
    'calSv-r14': { datatype: 'u64', store: '[ rsp - 0x60 ]' },
    'calSv-r15': { datatype: 'u64', store: '[ rsp - 0x58 ]' },
    'calSv-rbp': { datatype: 'u64', store: '[ rsp - 0x78 ]' },
    'calSv-rbx': { datatype: 'u64', store: '[ rsp - 0x80 ]' },
    out1: { datatype: 'u64[4]', store: '[ rsp - 0x50 ]' },
    x106: { datatype: 'u64', store: 'r15' },
    x107: { datatype: 'u64', store: '[ rsp - 0x10 ]' },
    x22: { datatype: 'u64', store: '[ rsp - 0x18 ]' },
    x38: { datatype: 'u1', store: 'OF' },
    x39: { datatype: 'u64', store: '[ rsp - 0x40 ]' },
    x40: { datatype: 'u64', store: '[ rsp - 0x48 ]' },
    x41: { datatype: 'u64', store: '[ rsp - 0x20 ]' },
    x42: { datatype: 'u64', store: '[ rsp - 0x38 ]' },
    x51: { datatype: 'u64', store: 'rcx' },
    x53: { datatype: 'u64', store: 'r9' },
    x55: { datatype: 'u64', store: 'r12' },
    x57: { datatype: 'u64', store: 'r11' },
    x58: { datatype: 'u1', store: 'CF' },
    x66: { datatype: 'u64', store: 'rbp' },
    x68: { datatype: 'u1', store: 'dil' },
    x69: { datatype: 'u64', store: 'rdx' },
    x70: { datatype: 'u1', store: 'r8b' },
    x71: { datatype: 'u64', store: '[ rsp - 0x30 ]' },
    x72: { datatype: 'u64', store: '[ rsp - 0x28 ]' },
    x77: { datatype: 'u64', store: 'rbx' },
    x78: { datatype: 'u64', store: 'r13' },
    x96: { datatype: 'u64', store: 'r14' },
    x97: { datatype: 'u64', store: 'rax' }
  },
  pres: [
    '',
    ';should save OF(x38) but as it has not dependents, we just ignore it.'
  ],
  failfile: '/home/andreser/CryptOpt/results/lastFail.asm'
}
{
  curOperation: {
    datatype: 'u64',
    name: [ 'x59', '_' ],
    operation: 'addcarryx',
    arguments: [ 'x58', 'x38', 'x40' ],
    decisions: {
      di_choose_arg: [Array],
      di_spill_location: [Array],
      di_flag: [Array],
      di_handle_flags_kk: [Array],
      di_choose_imm: [Array]
    },
    decisionsHot: []
  },
  e: Error: tried to spill OF, but didnt work. TSNH.
      at Jt (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:24964)
      at pe (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:37026)
      at $e (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:33719)
      at Ae (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:51131)
      at file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:61683
      at Timeout._onTimeout (file:///home/andreser/CryptOpt/dist/CryptOpt.js:1:62312)
      at listOnTimeout (node:internal/timers:573:17)
      at process.processTimers (node:internal/timers:514:7),
  allocs: {
    '0x100000000': { datatype: 'u64', store: 'r10' },
    arg1: { datatype: 'u64[4]', store: 'rsi' },
    'calSv-r12': { datatype: 'u64', store: '[ rsp - 0x70 ]' },
    'calSv-r13': { datatype: 'u64', store: '[ rsp - 0x68 ]' },
    'calSv-r14': { datatype: 'u64', store: '[ rsp - 0x60 ]' },
    'calSv-r15': { datatype: 'u64', store: '[ rsp - 0x58 ]' },
    'calSv-rbp': { datatype: 'u64', store: '[ rsp - 0x78 ]' },
    'calSv-rbx': { datatype: 'u64', store: '[ rsp - 0x80 ]' },
    out1: { datatype: 'u64[4]', store: '[ rsp - 0x50 ]' },
    x106: { datatype: 'u64', store: 'r15' },
    x107: { datatype: 'u64', store: '[ rsp - 0x10 ]' },
    x22: { datatype: 'u64', store: '[ rsp - 0x18 ]' },
    x38: { datatype: 'u1', store: 'OF' },
    x39: { datatype: 'u64', store: '[ rsp - 0x40 ]' },
    x40: { datatype: 'u64', store: '[ rsp - 0x48 ]' },
    x41: { datatype: 'u64', store: '[ rsp - 0x20 ]' },
    x42: { datatype: 'u64', store: '[ rsp - 0x38 ]' },
    x51: { datatype: 'u64', store: 'rcx' },
    x53: { datatype: 'u64', store: 'r9' },
    x55: { datatype: 'u64', store: 'r12' },
    x57: { datatype: 'u64', store: 'r11' },
    x58: { datatype: 'u1', store: 'CF' },
    x66: { datatype: 'u64', store: 'rbp' },
    x68: { datatype: 'u1', store: 'dil' },
    x69: { datatype: 'u64', store: 'rdx' },
    x70: { datatype: 'u1', store: 'r8b' },
    x71: { datatype: 'u64', store: '[ rsp - 0x30 ]' },
    x72: { datatype: 'u64', store: '[ rsp - 0x28 ]' },
    x77: { datatype: 'u64', store: 'rbx' },
    x78: { datatype: 'u64', store: 'r13' },
    x96: { datatype: 'u64', store: 'r14' },
    x97: { datatype: 'u64', store: 'rax' }
  },
  pres: [
    '',
    ';should save OF(x38) but as it has not dependents, we just ignore it.'
  ],
  failfile: '/home/andreser/CryptOpt/results/lastFail.asm'
}

Done with code: 1 (statefile: /home/andreser/CryptOpt/results/manual/p256_sqr/seed0000000000000002.json)

Wrote RES/manual/p256_sqr/seed0000000000000002.json exiting.

It is possible that the input is silly, I haven't proven anything about it yet.
@dderjoel
Copy link
Collaborator

dderjoel commented Sep 13, 2023 •
edited
Loading

I think the problem is that there is no support for adding two carry bits with one 64 bit limb, when both of those bits are in CF and OF respectively.
Ilooking at the "lastFail.asm" file, It seems that it calculates x38 with adox, then x58 with adcx:

; fr__rm_rm_rmf x38 /* COUT */, x37, r11, r11, OF(u1) /* CarryIN */
	;why? OF ain't a flag, right?
	; in fr__r_rm_f
	adox r11, r11
	
	
	
	; fr__rm_rm_rmf x58 /* COUT */, x57, r11, [ rsp - 0x40 ], CF(u1) /* CarryIN */
	; in fr__r_rm_f
	adcx r11, [ rsp - 0x40 ]

And the next operation is then to add both of those flags to x40.
If I remember correctly, CryptOpt then tries to "spill one flag" into a register, and use the respective other adx instruction to add it to the limb. e.g. say x40 is in rax, then

seto bl
movzx rbx, bl
adcx rax, rbx

And the carry out is in CF, the result in rax.

Long story short, i believe its a bug in CryptOpt,

It surely is the offending operation.
I don't have time now (neither in the next couple weeks), but a (very bad) workaround for now would be to add an operation like this:

{
      "datatype": "u64",
      "name": ["x200"],
      "operation": "<<",
      "parameters": { "size": 64 },
      "arguments": ["x58", "0x0"]
    },

or

{
      "datatype": "u64",
      "name": ["x200"],
      "operation": "&",
      "parameters": { "size": 64 },
      "arguments": ["x58", "0x1"]
    },

and replace the "x58" in the operation that uses "x58" with "x200".

The reason why this is bad is that <<, ie. 'shl' kills both flags. I think & is a bit better, because it may be implemented with a bzhi or and and this clears instead of kills the flags... which may be a minor improvement.

I've locally tried "x58 + 0" but in no fiat function we ever had "addition with a constant", neither would "x200 = x58" work, because "="-operations are assumed to write to out1[0].

@andres-erbsen
Copy link
Author

As the output carry is unused, I believe the desired assembly code would be

adcx x40, zero
adox x40, zero

adc can take an immediate, but the adx versions cannot, so the zero would have to be in a a register or the memory. I think the human idiom is to zero the flags and a register using xor before starting the carry chain.

@dderjoel
Copy link
Collaborator

dderjoel commented Oct 4, 2023

that would be one way to do it, if there is a register with a zero available.
if not, I could think of

setc al
movzx rax, al
adox x40, rax

or, potentially

setc al
seto ah
popcnt ax,ax
movzx rax, ax
adc x40, rax

but that would require more support in many tools... So I'll try to fix it with the former.

@andres-erbsen
Copy link
Author

Sounds good, thanks! The first alternative seems fine. Another variant that may be worth trying:

mov rax, 0
adcx rax, rax
adox x40, rax

@dderjoel
Copy link
Collaborator

dderjoel commented Oct 5, 2023

The equivalence checker would accept both, right?

@andres-erbsen
Copy link
Author

Yep, I've been switching back and forth between these manually in cryptopt output.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@andres-erbsen @dderjoel