Merge pull request #76 from CertiCoq/joom/value-in-codegen

Codegen should use the `value` type instead of `unsigned long` or `unsigned long long`

benchmarks/.gitignore

@@ -8,6 +8,7 @@ Top.*
 glue.Top.*
 ffi.Top.*
 
+m.h
 gc.c
 gc.h
 gc_stack.c

benchmarks/Makefile

@@ -17,6 +17,7 @@ $(CFILES): tests
 exec: $(TESTS)
 
 copy:
+	cp ../theories/Runtime/m.h ./
 	cp ../theories/Runtime/gc.c ./
 	cp ../theories/Runtime/gc.h ./
 	cp ../theories/Runtime/gc_stack.c ./
@@ -27,6 +28,7 @@ copy:
 	cp ../theories/Runtime/mod.py ./
 
 clean:
+	rm -f ./m.h
 	rm -f ./gc.c
 	rm -f ./gc.h
 	rm -f ./gc_stack.c

benchmarks/basics.c

@@ -1,27 +1,10 @@
-#include "values.h"
+#include "gc_stack.h"
 struct closure;
-struct stack_frame;
-struct thread_info;
 struct closure {
   value (*func)(struct thread_info, value, value);
   value env;
 };
 
-struct stack_frame {
-  value *next;
-  value *root;
-  struct stack_frame *prev;
-};
-
-struct thread_info {
-  value *alloc;
-  value *limit;
-  struct heap *heap;
-  value args[1024];
-  struct stack_frame *fp;
-  unsigned long long nalloc;
-};
-
 extern int printf(signed char *);
 extern _Bool is_ptr(value);
 unsigned int get_unboxed_ordinal(value);
@@ -58,12 +41,12 @@ signed char const prop_lit[7] = { 60, 112, 114, 111, 112, 62, 0, };
 
 unsigned int get_unboxed_ordinal(value $v)
 {
-  return (unsigned long long) $v >> 1LL;
+  return (value) $v >> 1LL;
 }
 
 unsigned int get_boxed_ordinal(value $v)
 {
-  return *((unsigned long long *) $v + -1LL) & 255LL;
+  return *((value *) $v + -1LL) & 255LL;
 }
 
 value *get_args(value $v)
@@ -240,8 +223,8 @@ void print_Coq_Init_Datatypes_bool(value $v)
 
 value call(struct thread_info *$tinfo, value $clo, value $arg)
 {
-  register unsigned long long *$f;
-  register unsigned long long *$envi;
+  register value *$f;
+  register value *$envi;
   register value $tmp;
   $f = (*((struct closure *) $clo)).func;
   $envi = (*((struct closure *) $clo)).env;

benchmarks/basics.h

@@ -1,27 +1,10 @@
-#include "values.h"
+#include "gc_stack.h"
 struct closure;
-struct stack_frame;
-struct thread_info;
 struct closure {
   value (*func)(struct thread_info, value, value);
   value env;
 };
 
-struct stack_frame {
-  value *next;
-  value *root;
-  struct stack_frame *prev;
-};
-
-struct thread_info {
-  value *alloc;
-  value *limit;
-  struct heap *heap;
-  value args[1024];
-  struct stack_frame *fp;
-  unsigned long long nalloc;
-};
-
 extern unsigned int get_unboxed_ordinal(value);
 extern unsigned int get_boxed_ordinal(value);
 extern value *get_args(value);

benchmarks/binom_main.c

@@ -1,16 +1,11 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-extern void print_Coq_Init_Datatypes_nat(unsigned long long);
-
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern void print_Coq_Init_Datatypes_nat(value);
 
 int main(int argc, char *argv[]) {
   value val;

benchmarks/color_main.c

@@ -1,18 +1,13 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-extern void print_Coq_Numbers_BinNums_Z(unsigned long long);
-
-extern void print_Coq_Init_Datatypes_prod(unsigned long long, void (*)(unsigned long long), void (*)(unsigned long long));
+extern void print_Coq_Numbers_BinNums_Z(value);
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern void print_Coq_Init_Datatypes_prod(value, void (*)(value), void (*)(value));
 
 int main(int argc, char *argv[]) {
   value val;

benchmarks/demo1_main.c

@@ -1,18 +1,13 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-extern void print_Coq_Init_Datatypes_list(unsigned long long, void (*)(unsigned long long));
-
-extern void print_Coq_Init_Datatypes_bool(unsigned long long);
+extern void print_Coq_Init_Datatypes_list(value, void (*)(value));
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern void print_Coq_Init_Datatypes_bool(value);
 
 int main(int argc, char *argv[]) {
   value val;

benchmarks/demo2_main.c

@@ -1,6 +1,6 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
 
@@ -10,10 +10,6 @@ extern void print_Coq_Init_Datatypes_list(unsigned long long, void (*)(unsigned
 
 extern void print_Coq_Init_Datatypes_bool(unsigned long long);
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
-
 int main(int argc, char *argv[]) {
   value val;
   struct thread_info* tinfo;

benchmarks/demo3_main.c

@@ -1,23 +1,19 @@
 #include <stdio.h>
 #include <stdlib.h>
 #include <stdarg.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
 /* TODO: This should be imported with include. */
 extern value body(struct thread_info *);
 
 extern struct thread_info;
-extern void print_Coq_Init_Datatypes_list(unsigned long long, void (*)(unsigned long long));
-extern void print_Coq_Init_Datatypes_bool(unsigned long long);
-extern value get_Coq_Init_Datatypes_pair_args (unsigned long long);
+extern void print_Coq_Init_Datatypes_list(value, void (*)(value));
+extern void print_Coq_Init_Datatypes_bool(value);
+extern value get_Coq_Init_Datatypes_pair_args (value);
 extern value make_Coq_Init_Datatypes_bool_true (void);
 extern value make_Coq_Init_Datatypes_bool_false (void);
-extern void* call(struct thread_info *tinfo, unsigned long long clos, unsigned long long arg0);
-
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern value call(struct thread_info *tinfo, value clos, value arg0);
 
 value calls(struct thread_info* tinfo, value clos, unsigned int n, ...)
 {
@@ -26,7 +22,7 @@ value calls(struct thread_info* tinfo, value clos, unsigned int n, ...)
   va_start(args, n);
 
   for(; n != 0; n--) {
-    v = va_arg(args, unsigned long long);
+    v = va_arg(args, value);
     clos = call(tinfo, clos, v);
   }
   va_end(args);

benchmarks/list_sum_main.c

@@ -3,16 +3,9 @@
 #include "gc.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-extern void print_Coq_Init_Datatypes_nat(unsigned long long);
-
-extern value args[];
-
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern void print_Coq_Init_Datatypes_nat(value);
 
 int main(int argc, char *argv[]) {
   value val;

benchmarks/sha_fast_main.c

@@ -1,15 +1,10 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
-
 int main(int argc, char *argv[]) {
   value val;
   struct thread_info* tinfo;

benchmarks/test_primitive_main.c

@@ -1,15 +1,10 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
-
 int main(int argc, char *argv[]) {
   value val;
   struct thread_info* tinfo;

benchmarks/vs_easy_main.c

@@ -1,50 +1,39 @@
 #include <stdio.h>
 #include <stdlib.h>
-#include "gc.h"
+#include "gc_stack.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-extern void print_Coq_Init_Datatypes_bool(unsigned long long);
-
-extern void print_CertiCoq_Benchmarks_lib_vs_space_atom(unsigned long long);
+extern void print_Coq_Init_Datatypes_bool(value);
 
-extern unsigned int get_Coq_Init_Datatypes_list_tag(unsigned long long);
+extern void print_CertiCoq_Benchmarks_lib_vs_space_atom(value);
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern unsigned int get_Coq_Init_Datatypes_list_tag(value);
 
-extern void print_Coq_Init_Datatypes_list(unsigned long long, void (*)(unsigned long long));
+extern void print_Coq_Init_Datatypes_list(value, void (*)(value));
 
-extern void print_CertiCoq_Benchmarks_lib_vs_clause(unsigned long long);
+extern void print_CertiCoq_Benchmarks_lib_vs_clause(value);
 
-void print_elem(unsigned long long v)
-{
+void print_elem(value v) {
   printf(".");
 }
 
-void print_list(unsigned long long l)
-{
+void print_list(value l) {
   print_Coq_Init_Datatypes_list(l, print_elem);
   printf("\n");
 }
 
-void print_list_space_atom(unsigned long long l)
-{
+void print_list_space_atom(value l) {
   print_Coq_Init_Datatypes_list(l, print_CertiCoq_Benchmarks_lib_vs_space_atom);
   printf("\n");
 }
 
-void print_list_clause(unsigned long long l)
-{
+void print_list_clause(value l) {
   print_Coq_Init_Datatypes_list(l, print_CertiCoq_Benchmarks_lib_vs_clause);
   printf("\n");
 }
 
-
-
 int main(int argc, char *argv[]) {
   value val;
   struct thread_info* tinfo;

benchmarks/vs_hard_main.c

@@ -3,29 +3,21 @@
 #include "gc.h"
 #include <time.h>
 
-
 extern value body(struct thread_info *);
 
-extern void print_Coq_Init_Datatypes_bool(unsigned long long);
-
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
+extern void print_Coq_Init_Datatypes_bool(value);
 
-extern void print_Coq_Init_Datatypes_list(unsigned long long, void (*)(unsigned long long));
+extern void print_Coq_Init_Datatypes_list(value, void (*)(value));
 
-void print_elem(unsigned long long v)
-{
+void print_elem(value v) {
   printf(".");
 }
 
-void print_list(unsigned long long l)
-{
+void print_list(value l) {
   print_Coq_Init_Datatypes_list(l, print_elem);
   printf("\n");
 }
 
-
 int main(int argc, char *argv[]) {
   value val;
   struct thread_info* tinfo;

bootstrap/certicoqc/certicoqc_wrapper.c

@@ -1,19 +1,15 @@
 #include <stdio.h>
 #include <stdlib.h>
+#include "values.h"
 #include "gc.h"
 #include <caml/memory.h>
 #include <time.h>
-#include <caml/mlvalues.h>
 #include <caml/callback.h>
 
 extern value body(struct thread_info *);
 
 extern value *call(struct thread_info *, value, value);
 
-_Bool is_ptr(value s) {
-  return (_Bool) Is_block(s);
-}
-
 // external certicoq_pipeline : (coq_Options × ExtractedASTBaseQuoter.quoted_program) -> coq_Cprogram error * Bytestring.String.t = "certicoq_pipeline"
 CAMLprim value certicoq_pipeline_wrapper(value opts, value prog) {
   CAMLparam2 (opts, prog);