Merge pull request #738 from CakeML/export_update

Export update

basis/basis_ffi.c

@@ -19,9 +19,14 @@
 
 /* clFFI (command line) */
 
-/* argc and argv are exported in cake.S */
-extern unsigned int argc;
-extern char **argv;
+unsigned int argc;
+char **argv;
+
+/* exported in cake.S */
+extern void cml_main(void);
+extern void *cml_heap;
+extern void *cml_stack;
+extern void *cml_stackend;
 
 void ffiget_arg_count (unsigned char *c, long clen, unsigned char *a, long alen) {
  a[0] = (char) argc;
@@ -247,3 +252,62 @@ void ffidouble_toString (unsigned char *c, long clen, unsigned char *a, long ale
  // for the 0 byte
  assert (bytes_written <= 255);
 }
+
+void main (int local_argc, char **local_argv) {
+
+ argc = local_argc;
+ argv = local_argv;
+
+ char *heap_env = getenv("CML_HEAP_SIZE");
+ char *stack_env = getenv("CML_STACK_SIZE");
+ char *temp; //used to store remainder of strtoul parse
+
+ unsigned long sz = 1024*1024; // 1 MB unit
+ unsigned long cml_heap_sz = 1024 * sz; // Default: 1 GB heap
+ unsigned long cml_stack_sz = 1024 * sz; // Default: 1 GB stack
+
+ // Read CML_HEAP_SIZE env variable (if present)
+ // Warning: strtoul may overflow!
+ if(heap_env != NULL)
+ {
+ cml_heap_sz = strtoul(heap_env, &temp, 10);
+ cml_heap_sz *= sz; //heap size is read in units of MBs
+ }
+
+ if(stack_env != NULL)
+ {
+ cml_stack_sz = strtoul(stack_env, &temp, 10);
+ cml_stack_sz *= sz; //stack size is read in units of MBs
+ }
+
+ if(cml_heap_sz < sz || cml_stack_sz < sz) //At least 1MB heap and stack size
+ {
+ #ifdef STDERR_MEM_EXHAUST
+ fprintf(stderr,"Too small requested heap (%lu) or stack (%lu) size in bytes.\n",cml_heap_sz, cml_stack_sz);
+ #endif
+ exit(3);
+ }
+
+ if(cml_heap_sz + cml_stack_sz < cml_heap_sz)
+ {
+ #ifdef STDERR_MEM_EXHAUST
+ fprintf(stderr,"Overflow in requested heap (%lu) + stack (%lu) size in bytes.\n",cml_heap_sz, cml_stack_sz);
+ #endif
+ exit(3);
+ }
+
+ cml_heap = malloc(cml_heap_sz + cml_stack_sz); // allocate both heap and stack at once
+
+ if(cml_heap == NULL)
+ {
+ #ifdef STDERR_MEM_EXHAUST
+ fprintf(stderr,"malloc() failed to allocate sufficient CakeML heap and stack space.\n");
+ #endif
+ exit(3);
+ }
+
+ cml_stack = cml_heap + cml_heap_sz;
+ cml_stackend = cml_stack + cml_stack_sz;
+
+ cml_main(); // Passing control to CakeML
+}

candle/standard/opentheory/compilation/ag32/readerCompileScript.sml

@@ -7,6 +7,6 @@ open preamble compilationLib readerProgTheory
 val _ = new_theory "readerCompile"
 
 val reader_compiled = save_thm ("reader_compiled",
- compile_ag32 500 500 "reader" reader_prog_def);
+ compile_ag32 "reader" reader_prog_def);
 
 val _ = export_theory ();

candle/standard/opentheory/compilation/readerCompileScript.sml

@@ -7,6 +7,6 @@ open x64_configTheory
 val _ = new_theory "readerCompile"
 
 val reader_compiled = save_thm("reader_compiled",
- compile_x64 1000 1000 "reader" reader_prog_def);
+ compile_x64 "reader" reader_prog_def);
 
 val _ = export_theory ();

candle/standard/opentheory/monadIO/compilation/readerIOCompileScript.sml

@@ -6,6 +6,6 @@ open preamble compilationLib readerIOProgTheory
 val _ = new_theory "readerIOCompile"
 
 val readerIO_compiled = save_thm("readerIO_compiled",
- compile_x64 1000 1000 "readerIO" readerIO_prog_def);
+ compile_x64 "readerIO" readerIO_prog_def);
 
 val _ = export_theory ();

compiler/backend/ag32/export_ag32Script.sml

@@ -6,8 +6,7 @@ open preamble exportTheory
 val () = new_theory "export_ag32";
 
 val ag32_export_def = Define `
- ag32_export (ffi_names:string list) (heap_space:num) (stack_space:num)
- bytes (data:word32 list) =
+ ag32_export (ffi_names:string list) bytes (data:word32 list) =
  SmartAppend
  (split16 (words_line (strlit".data_word ") word_to_string) data)
  (split16 (words_line (strlit".code_byte ") byte_to_string) bytes)`;

compiler/backend/arm7/export_arm7Script.sml

@@ -5,26 +5,35 @@ open preamble exportTheory
 
 val () = new_theory "export_arm7";
 
+(*
+CakeML expects 4 arguments in order:
+
+r0 - entry address i.e., the address of cake_main
+r1 - first address of heap
+r2 - first address of stack
+r3 - first address past the stack
+
+In addition, the first address on the heap should store the address of cake_bitmaps
+
+Note: this set up does NOT account for restoring clobbered registers
+*)
 val startup =
  ``(MAP (\n. strlit(n ++ "\n"))
  ["/* Start up code */";
  "";
  " .text";
  " .p2align 3";
- " .globl cdecl(main)";
- " .globl cdecl(argc)";
- " .globl cdecl(argv)";
- "cdecl(main):";
- " ldr r2,=cdecl(argc)";
- " ldr r3,=cdecl(argv)";
- " str r0,[r2]";
- " str r1,[r3]";
- " ldr r0,=cake_main";
- " ldr r1,=cake_heap";
+ " .globl cdecl(cml_main)";
+ " .globl cdecl(cml_heap)";
+ " .globl cdecl(cml_stack)";
+ " .globl cdecl(cml_stackend)";
+ "cdecl(cml_main):";
+ " ldr r0,=cake_main /* arg1: entry address */";
+ " ldr r1,=cdecl(cml_heap) /* arg2: first address of heap */";
  " ldr r2,=cake_bitmaps";
- " str r2,[r1]";
- " ldr r2,=cake_stack";
- " ldr r3,=cake_end";
+ " str r2,[r1] /* store bitmap pointer */";
+ " ldr r2,=cdecl(cml_stack) /* arg3: first address of stack */";
+ " ldr r3,=cdecl(cml_stackend) /* arg4: first address past the stack */ ";
  " b cake_main";
  " .ltorg";
  ""])`` |> EVAL |> concl |> rand
@@ -62,10 +71,10 @@ val ffi_code =
  ""])))`` |> EVAL |> concl |> rand
 
 val arm7_export_def = Define `
- arm7_export ffi_names heap_space stack_space bytes (data:word32 list) =
+ arm7_export ffi_names bytes (data:word32 list) =
  SmartAppend
  (SmartAppend (List preamble)
- (SmartAppend (List (data_section ".long" heap_space stack_space))
+ (SmartAppend (List (data_section ".long"))
  (SmartAppend (split16 (words_line (strlit"\t.long ") word_to_string) data)
  (SmartAppend (List ((strlit"\n")::^startup)) ^ffi_code))))
  (split16 (words_line (strlit"\t.byte ") byte_to_string) bytes)`;

compiler/backend/arm8/export_arm8Script.sml

@@ -5,26 +5,35 @@ open preamble exportTheory
 
 val () = new_theory "export_arm8";
 
+(*
+CakeML expects 4 arguments in order:
+
+x0 - entry address i.e., the address of cake_main
+x1 - first address of heap
+x2 - first address of stack
+x3 - first address past the stack
+
+In addition, the first address on the heap should store the address of cake_bitmaps
+
+Note: this set up does NOT account for restoring clobbered registers
+*)
 val startup =
  ``(MAP (\n. strlit(n ++ "\n"))
  ["/* Start up code */";
  "";
  " .text";
  " .p2align 3";
- " .globl cdecl(main)";
- " .globl cdecl(argc)";
- " .globl cdecl(argv)";
- "cdecl(main):";
- " ldr x2,=cdecl(argc)";
- " ldr x3,=cdecl(argv)";
- " str x0,[x2]";
- " str x1,[x3]";
- " ldr x0,=cake_main";
- " ldr x1,=cake_heap";
+ " .globl cdecl(cml_main)";
+ " .globl cdecl(cml_heap)";
+ " .globl cdecl(cml_stack)";
+ " .globl cdecl(cml_stackend)";
+ "cdecl(cml_main):";
+ " ldr x0,=cake_main /* arg1: entry address */";
+ " ldr x1,=cdecl(cml_heap) /* arg2: first address of heap */";
  " ldr x2,=cake_bitmaps";
- " str x2,[x1]";
- " ldr x2,=cake_stack";
- " ldr x3,=cake_end";
+ " str x2,[x1] /* store bitmap pointer */";
+ " ldr x2,=cdecl(cml_stack) /* arg3: first address of stack */";
+ " ldr x3,=cdecl(cml_stackend) /* arg4: first address past the stack */ ";
  " b cake_main";
  " .ltorg";
  ""])`` |> EVAL |> concl |> rand
@@ -62,10 +71,10 @@ val ffi_code =
  ""])))`` |> EVAL |> concl |> rand
 
 val arm8_export_def = Define `
- arm8_export ffi_names heap_space stack_space bytes (data:word64 list) =
+ arm8_export ffi_names bytes (data:word64 list) =
  SmartAppend
  (SmartAppend (List preamble)
- (SmartAppend (List (data_section ".quad" heap_space stack_space))
+ (SmartAppend (List (data_section ".quad"))
  (SmartAppend (split16 (words_line (strlit"\t.quad ") word_to_string) data)
  (SmartAppend (List ((strlit"\n")::^startup)) ^ffi_code))))
  (split16 (words_line (strlit"\t.byte ") byte_to_string) bytes)`;

compiler/backend/exportScript.sml

@@ -37,27 +37,13 @@ val preamble_tm =
  ""])`` |> EVAL |> rconc;
 val preamble_def = Define`preamble = ^preamble_tm`;
 
-val space_line_def = Define`
- space_line n = concat[strlit" .space 1024 * 1024 * "; toString (n:num); strlit "\n"]`;
-
-val data_section_def = Define`data_section word_directive heap_space stack_space =
- MAP (\n. strlit (n ++ "\n"))
- ["/* Data section -- modify the numbers to change stack/heap size */";
- "";
- " .bss";
- " .p2align 3";
- "cake_heap:"] ++ [space_line heap_space] ++
+val data_section_def = Define`data_section word_directive =
  MAP (\n. strlit (n ++ "\n"))
- [" .p2align 3";
- "cake_stack:"] ++ [space_line stack_space] ++
- MAP (\n. (strlit (n ++ "\n")))
- [" .p2align 3";
- "cake_end:";
- "";
- " .data";
+ [" .data";
  " .p2align 3";
- "cdecl(argc): " ++ word_directive ++ " 0";
- "cdecl(argv): " ++ word_directive ++ " 0";
+ "cdecl(cml_heap): " ++ word_directive ++ " 0";
+ "cdecl(cml_stack): " ++ word_directive ++ " 0";
+ "cdecl(cml_stackend): " ++ word_directive ++ " 0";
  " .p2align 3";
  "cake_bitmaps:"]`;
 

compiler/backend/mips/export_mipsScript.sml

@@ -5,27 +5,35 @@ open preamble exportTheory
 
 val () = new_theory "export_mips";
 
+(*
+CakeML expects 4 arguments in order:
+
+a0 - entry address i.e., the address of cake_main
+a1 - first address of heap
+a2 - first address of stack
+a3 - first address past the stack
+
+In addition, the first address on the heap should store the address of cake_bitmaps
+
+Note: this set up does NOT account for restoring clobbered registers
+*)
 val startup =
  ``(MAP (\n. strlit(n ++ "\n"))
  ["#### Start up code";
  "";
  " .text";
  " .p2align 3";
- " .globl cdecl(main)";
- " .globl cdecl(argc)";
- " .globl cdecl(argv)";
- "";
- "cdecl(main):";
- " dla $t0,cdecl(argc)";
- " dla $t1,cdecl(argv)";
- " sd $a0, 0($t0) # a0 stores argc";
- " sd $a1, 0($t1) # a1 stores argv";
- " dla $a0,cake_main # arg1: entry address";
- " dla $a1,cake_heap # arg2: first address of heap";
+ " .globl cdecl(cml_main)";
+ " .globl cdecl(cml_heap)";
+ " .globl cdecl(cml_stack)";
+ " .globl cdecl(cml_stackend)";
+ "cdecl(cml_main):";
+ " dla $a0,cake_main # arg1: entry address";
+ " dla $a1,cdecl(cml_heap) # arg2: first address of heap";
  " dla $t0,cake_bitmaps";
- " sd $t0, 0($a1) # store bitmap pointer";
- " dla $a2,cake_stack # arg3: first address of stack";
- " dla $a3,cake_end  # arg4: first address past the stack";
+ " sd $t0, 0($a1)  # store bitmap pointer";
+ " dla $a2,cdecl(cml_stack)  # arg3: first address of stack";
+ " dla $a3,cdecl(cml_stackend) # arg4: first address past the stack";
  " j cake_main";
  " nop";
  ""])`` |> EVAL |> concl |> rand
@@ -66,10 +74,10 @@ val ffi_code =
  ""])))`` |> EVAL |> concl |> rand
 
 val mips_export_def = Define `
- mips_export ffi_names heap_space stack_space bytes (data:word64 list) =
+ mips_export ffi_names bytes (data:word64 list) =
  SmartAppend
  (SmartAppend (List preamble)
- (SmartAppend (List (data_section ".quad" heap_space stack_space))
+ (SmartAppend (List (data_section ".quad"))
  (SmartAppend (split16 (words_line (strlit"\t.quad ") word_to_string) data)
  (SmartAppend (List ((strlit"\n")::^startup)) ^ffi_code))))
  (split16 (words_line (strlit"\t.byte ") byte_to_string) bytes)`;

compiler/backend/riscv/export_riscvScript.sml

@@ -5,27 +5,35 @@ open preamble exportTheory
 
 val () = new_theory "export_riscv";
 
+(*
+CakeML expects 4 arguments in order:
+
+a0 - entry address i.e., the address of cake_main
+a1 - first address of heap
+a2 - first address of stack
+a3 - first address past the stack
+
+In addition, the first address on the heap should store the address of cake_bitmaps
+
+Note: this set up does NOT account for restoring clobbered registers
+*)
 val startup =
  ``(MAP (\n. strlit(n ++ "\n"))
  ["#### Start up code";
  "";
  " .text";
  " .p2align 3";
- " .globl cdecl(main)";
- " .globl cdecl(argc)";
- " .globl cdecl(argv)";
- "";
- "cdecl(main):";
- " la t3,cdecl(argc)";
- " la x4,cdecl(argv)";
- " sd a0, 0(t3) # a0 stores argc";
- " sd a1, 0(x4) # a1 stores argv";
- " la a0,cake_main # arg1: entry address";
- " la a1,cake_heap # arg2: first address of heap";
+ " .globl cdecl(cml_main)";
+ " .globl cdecl(cml_heap)";
+ " .globl cdecl(cml_stack)";
+ " .globl cdecl(cml_stackend)";
+ "cdecl(cml_main):";
+ " la a0,cake_main # arg1: entry address";
+ " la a1,cdecl(cml_heap) # arg2: first address of heap";
  " la t3,cake_bitmaps";
- " sd t3, 0(a1) # store bitmap pointer";
- " la a2,cake_stack # arg3: first address of stack";
- " la a3,cake_end  # arg4: first address past the stack";
+ " sd t3, 0(a1)  # store bitmap pointer";
+ " la a2,cdecl(cml_stack)  # arg3: first address of stack";
+ " la a3,cdecl(cml_stackend) # arg4: first address past the stack";
  " j cake_main";
  ""])`` |> EVAL |> concl |> rand
 
@@ -65,10 +73,10 @@ val ffi_code =
  ""])))`` |> EVAL |> concl |> rand
 
 val riscv_export_def = Define `
- riscv_export ffi_names heap_space stack_space bytes (data:word64 list) =
+ riscv_export ffi_names bytes (data:word64 list) =
  SmartAppend
  (SmartAppend (List preamble)
- (SmartAppend (List (data_section ".quad" heap_space stack_space))
+ (SmartAppend (List (data_section ".quad"))
  (SmartAppend (split16 (words_line (strlit"\t.quad ") word_to_string) data)
  (SmartAppend (List ((strlit"\n")::^startup)) ^ffi_code))))
  (split16 (words_line (strlit"\t.byte ") byte_to_string) bytes)`;