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

[Magnus Myreen]

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