From a90b94b43e5d1ff99effc6af306987b5f559871b Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Fri, 1 Jul 2016 11:04:43 +0200
Subject: add missing asmexpand step to cminor handler in driver

---
 driver/Driver.ml | 48 +++++++++++++++++++++++++++---------------------
 1 file changed, 27 insertions(+), 21 deletions(-)

diff --git a/driver/Driver.ml b/driver/Driver.ml
index 7311215d..a0ec07f1 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -86,29 +86,35 @@ let compile_cminor_file ifile ofile =
   Sections.initialize();
   let ic = open_in ifile in
   let lb = Lexing.from_channel ic in
-  try
-    match Compiler.transf_cminor_program
-            (CMtypecheck.type_program
-              (CMparser.prog CMlexer.token lb)) with
+  (* Parse cminor *)
+  let cm =
+    try CMtypecheck.type_program (CMparser.prog CMlexer.token lb)
+    with Parsing.Parse_error ->
+           eprintf "File %s, character %d: Syntax error\n"
+                   ifile (Lexing.lexeme_start lb);
+           exit 2
+       | CMlexer.Error msg ->
+           eprintf "File %s, character %d: %s\n"
+                   ifile (Lexing.lexeme_start lb) msg;
+           exit 2
+       | CMtypecheck.Error msg ->
+           eprintf "File %s, type-checking error:\n%s"
+                   ifile msg;
+           exit 2 in
+  (* Convert to Asm *)
+  let asm =
+    match Compiler.apply_partial
+               (Compiler.transf_cminor_program cm)
+               Asmexpand.expand_program with
+    | Errors.OK asm ->
+        asm
     | Errors.Error msg ->
         eprintf "%s: %a" ifile print_error msg;
-        exit 2
-    | Errors.OK p ->
-        let oc = open_out ofile in
-        PrintAsm.print_program oc p;
-        close_out oc
-  with Parsing.Parse_error ->
-         eprintf "File %s, character %d: Syntax error\n"
-                 ifile (Lexing.lexeme_start lb);
-         exit 2
-     | CMlexer.Error msg ->
-         eprintf "File %s, character %d: %s\n"
-                 ifile (Lexing.lexeme_start lb) msg;
-         exit 2
-     | CMtypecheck.Error msg ->
-         eprintf "File %s, type-checking error:\n%s"
-                 ifile msg;
-         exit 2
+        exit 2 in
+  (* Print Asm in text form *)
+  let oc = open_out ofile in
+  PrintAsm.print_program oc asm;
+  close_out oc
 
 (* Processing of a .c file *)
 
-- 
cgit 


From 948f5c7899acd1ecd1a948bd54b695c6fa3afafb Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Fri, 1 Jul 2016 11:05:39 +0200
Subject: extend cminor parser to accept "extern runtime" declarations

---
 backend/CMparser.mly | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 7fa6500a..94b50810 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -38,6 +38,8 @@ let mkef sg toks =
       EF_external(coqstring_of_camlstring s, sg)
   | [EFT_tok "builtin"; EFT_string s] ->
       EF_builtin(coqstring_of_camlstring s, sg)
+  | [EFT_tok "runtime"; EFT_string s] ->
+      EF_runtime(coqstring_of_camlstring s, sg)
   | [EFT_tok "volatile"; EFT_tok "load"; EFT_chunk c] ->
       EF_vload c
   | [EFT_tok "volatile"; EFT_tok "store"; EFT_chunk c] ->
@@ -348,6 +350,7 @@ let mkmatch expr cases =
 %token READONLY
 %token RETURN
 %token RPAREN
+%token RUNTIME
 %token SEMICOLON
 %token SINGLE
 %token SINGLEOFINT
@@ -719,6 +722,7 @@ eftok:
   | VOLATILE                                    { EFT_tok "volatile" }
   | EXTERN                                      { EFT_tok "extern" }
   | BUILTIN                                     { EFT_tok "builtin" }
+  | RUNTIME                                     { EFT_tok "runtime" }
   | memory_chunk                                { EFT_chunk $1 }
 ;
 
-- 
cgit 


From 2ef43e7647ccd65a2a8f1d9fdd067a18e52c39cb Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Fri, 1 Jul 2016 14:40:30 +0200
Subject: add 'runtime' token to lexer

---
 backend/CMlexer.mll | 1 +
 1 file changed, 1 insertion(+)

diff --git a/backend/CMlexer.mll b/backend/CMlexer.mll
index c82f5401..65f244b5 100644
--- a/backend/CMlexer.mll
+++ b/backend/CMlexer.mll
@@ -136,6 +136,7 @@ rule token = parse
   | "]"    { RBRACKET }
   | "readonly" { READONLY }
   | "return"    { RETURN }
+  | "runtime"    { RUNTIME }
   | ")"    { RPAREN }
   | ";"    { SEMICOLON }
   | "/"    { SLASH }
-- 
cgit