[CakeML-Dev] [CakeML/cakeml] b835dc: Move asm_ok up to word_to_stack

[Magnus Myreen]

Would we really need to use a new register? If at all possible, we
should try to avoid it because getting asm_ok to fail for one of these
is extremely rare (when does one have an enormous stack frame?).

Could we try to get through this without another reserved register,
e.g. StackLoad could load the constant in the register it'll update
with the load. If I remember correctly, StackStore will only be used
in places where one of the word_to_stack vars are unused. Similarly,
StackFree is used only in places where at least one of the reserved
variables is unused. This suggests that word_to_stack should
potentially decide how stack_remove is to use temporaries.

Cheers,
Magnus

On 17 October 2016 at 15:19, Yong Kiam <tanyongkiam at gmail.com> wrote:
> I think all three can be implemented most cleanly in stack_remove by
> offloading the constant into a register when it is too big but that will
> require an extra reserved register.
>
> On Mon, Oct 17, 2016 at 4:38 AM, Magnus Myreen <magnus.myreen at gmail.com>
> wrote:
>>
>> The following commit contains a comment:
>>
>>     need to assume something on all stack lookup/store sizes?
>>
>> I don't think there should be. Instead the implementation should break
>> problematic stack load/store/shrinks into multiple instructions, eg if
>>
>> store arg, [sp+40000]
>>
>> is not encodable, then do something like:
>>
>> add sp, 20000
>> add sp, 20000
>> store arg, [sp]
>> sub sp, 20000
>> sub sp, 20000
>>
>> Is this possible?
>>
>> Cheers,
>> Magnus
>>
>> ---------- Forwarded message ---------
>> From: GitHub <noreply at github.com>
>> Date: Mon, 17 Oct 2016 at 07:13
>> Subject: [CakeML/cakeml] b835dc: Move asm_ok up to word_to_stack
>> To: <commits at cakeml.org>
>>
>>
>>   Branch: refs/heads/asm_ok
>>   Home:   https://github.com/CakeML/cakeml
>>   Commit: b835dc96e0442cc883b47044e01fd492253c0244
>>
>> https://github.com/CakeML/cakeml/commit/b835dc96e0442cc883b47044e01fd492253c0244
>>   Author: Yong Kiam <tanyongkiam at gmail.com>
>>   Date:   2016-10-17 (Mon, 17 Oct 2016)
>>
>>   Changed paths:
>>     M compiler/backend/lab_to_targetScript.sml
>>     M compiler/backend/proofs/stack_to_labProofScript.sml
>>     M compiler/backend/semantics/labPropsScript.sml
>>
>>   Log Message:
>>   -----------
>>   Move asm_ok up to word_to_stack
>> - there are 3 probably unprovable cheats to do with over sized stack
>> arguments
>>
>>
>> _______________________________________________
>> Commits mailing list
>> Commits at cakeml.org
>> https://lists.cakeml.org/listinfo/commits
>
>