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

Yong Kiam tanyongkiam at gmail.com
Mon Oct 17 13:19:44 UTC 2016


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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161017/4fe16431/attachment.html>


More information about the Developers mailing list