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

[Yong Kiam]

In that case, I think word_to_stack can just re-use StackStoreAny and
StackLoadAny. Maybe a new StackFreeAny primitive should be added too.

On Mon, Oct 17, 2016 at 9:33 AM, Magnus Myreen <magnus.myreen at gmail.com>
wrote:

> 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/b835dc96e0442cc883b47044e01fd4
> 92253c0244
> >>   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/70dd1928/attachment.html>