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

[Yong Kiam]

Hmm, I want to minimize the stuff I add to word_to_stack.

I think the StackFreeAny/StackLoadAny will have to go in there with extra
state threaded through, but I think the consecutive StackFree can be
implemented later on in stack_remove (which is where StackAlloc is split up
as well). Does that sound right to you?

On Tue, Oct 18, 2016 at 10:47 AM, Magnus Myreen <magnus.myreen at gmail.com>
wrote:

> > In that case, I think word_to_stack can just re-use StackStoreAny and
> > StackLoadAny.
>
> Sounds good.
>
> > Maybe a new StackFreeAny primitive should be added too.
>
> Or maybe just use consecutive StackFree calls, just like we do for
> stack allocation for huge stack frames.
>
> Cheers,
> Magnus
>
> > 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/
> 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/20161018/57ab8d1a/attachment-0001.html>