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

Magnus Myreen magnus.myreen at gmail.com
Tue Oct 18 15:03:23 UTC 2016


On 18 October 2016 at 16:56, Yong Kiam <tanyongkiam at gmail.com> wrote:
> Hmm, I want to minimize the stuff I add to word_to_stack.

Yes, it's complicated enough as it is.

> 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?

Sounds good.

> 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
>> >> >
>> >> >
>> >
>> >
>
>



More information about the Developers mailing list