From ff40ff40ee967f6fd9206ef8c86426b0ea33cbde Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 14 Feb 2020 21:02:44 +0000
Subject: Update driver

---
 example/main.c       |  9 ++++++
 example/main.v       | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 extraction/driver.ml | 66 +++++++++++++++++++++++++++++++++++++++----
 lib/CompCert         |  2 +-
 4 files changed, 149 insertions(+), 7 deletions(-)
 create mode 100644 example/main.c
 create mode 100644 example/main.v

diff --git a/example/main.c b/example/main.c
new file mode 100644
index 0000000..6bd3334
--- /dev/null
+++ b/example/main.c
@@ -0,0 +1,9 @@
+int main() {
+    int x;
+    int y;
+    int z;
+    y = 2;
+    z = 3;
+    x = y * z;
+    return x;
+}
diff --git a/example/main.v b/example/main.v
new file mode 100644
index 0000000..63130fe
--- /dev/null
+++ b/example/main.v
@@ -0,0 +1,79 @@
+// -*- mode: verilog -*-
+
+module main(input start, reset, clk, 
+            output finished, output [31:0] return_val);
+
+   reg [31:0]      x;
+   reg [31:0]      y;
+   reg [31:0]      z;
+   reg [2:0]       state;
+
+   reg [31:0]     return_val_w;
+   reg            finished_w;
+
+   localparam [2:0] START_STATE = 0;
+   localparam [2:0] MAIN_STATE_0 = 1;
+   localparam [2:0] MAIN_STATE_1 = 2;
+   localparam [2:0] MAIN_STATE_2 = 3;
+   localparam [2:0] MAIN_STATE_3 = 4;
+   localparam [2:0] MAIN_STATE_4 = 5;
+   localparam [2:0] FINISHED_STATE = 6;
+
+   assign return_val = return_val_w;
+   assign finished = finished_w;
+
+   always @(posedge clk)
+     if (reset) begin
+        state <= START_STATE;
+        return_val_w <= 0;
+        finished_w <= 0;
+     end
+     else
+       case (state)
+         START_STATE: x <= 0;
+         MAIN_STATE_0: y <= 0;
+         MAIN_STATE_1: z <= 0;
+         MAIN_STATE_2: y <= 2;
+         MAIN_STATE_3: z <= 3;
+         MAIN_STATE_4: x <= y * z;
+         FINISHED_STATE: begin 
+            return_val_w <= x;
+            finished_w <= 1;
+         end
+         default: state <= START_STATE;
+       endcase
+
+   always @(posedge clk)
+     if (state != FINISHED_STATE)
+       state <= state + 1;
+
+endmodule
+
+module testbench;
+   reg start, reset, clk;
+   wire finished;
+   wire [31:0] return_val;
+   
+   main main(start, reset, clk, finished, return_val);
+
+   initial begin
+      $dumpvars;
+      start = 0;
+      reset = 1;
+      clk = 0;
+
+      @(posedge clk) begin
+         reset = 0;
+         start = 1;
+      end
+      @(posedge clk) start = 0;
+
+      #100;
+
+      $display("Result: %d", return_val);
+      $finish;
+   end
+
+   always #5 clk = ~clk;
+
+endmodule
diff --git a/extraction/driver.ml b/extraction/driver.ml
index f14a876..eb14d45 100644
--- a/extraction/driver.ml
+++ b/extraction/driver.ml
@@ -1,10 +1,12 @@
-(* let parse_c_file sourcename ifile =
+open Compcert
+
+let parse_c_file sourcename ifile =
   (* Simplification options *)
   let simplifs =
     "b" (* blocks: mandatory *)
-  ^ (if false then "s" else "")
-  ^ (if false then "f" else "")
-  ^ (if false then "p" else "")
+    ^ (if false then "s" else "")
+    ^ (if false then "f" else "")
+    ^ (if false then "p" else "")
   in
   (* Parsing and production of a simplified C AST *)
   let ast = Parse.preprocessed_file simplifs sourcename ifile in
@@ -13,7 +15,59 @@
   (* Save CompCert C AST if requested *)
   PrintCsyntax.print_if csyntax;
   csyntax
- *)
-open Compcert.Allocation
+
+let compile_c_file sourcename ifile ofile =
+  (* Parse the ast *)
+  let csyntax = parse_c_file sourcename ifile in
+  (* Convert to Asm *)
+  let rtl =
+    match Compiler.apply_partial
+            (CoqUp.transf_frontend csyntax) with
+    | Errors.OK rtl ->
+       rtl
+    | Errors.Error msg ->
+       let loc = file_loc sourcename in
+       fatal_error loc "%a"  print_error msg in
+  (* Print Asm in text form *)
+  let oc = open_out ofile in
+  PrintAsm.print_program oc asm;
+  close_out oc
+
+let compile_i_file sourcename preproname =
+  if !option_interp then begin
+      Machine.config := Machine.compcert_interpreter !Machine.config;
+      let csyntax = parse_c_file sourcename preproname in
+      Interp.execute csyntax;
+      ""
+    end else if !option_S then begin
+      compile_c_file sourcename preproname
+        (output_filename ~final:true sourcename ".c" ".s");
+      ""
+    end else begin
+      let asmname =
+        if !option_dasm
+        then output_filename sourcename ".c" ".s"
+        else tmp_file ".s" in
+      compile_c_file sourcename preproname asmname;
+      let objname = object_filename sourcename ".c" in
+      assemble asmname objname;
+      objname
+    end
+
+(* Processing of a .c file *)
+
+let process_c_file sourcename =
+  ensure_inputfile_exists sourcename;
+  if !option_E then begin
+      preprocess sourcename (output_filename_default "-");
+      ""
+    end else begin
+      let preproname = if !option_dprepro then
+                         output_filename sourcename ".c" ".i"
+                       else
+                         tmp_file ".i" in
+      preprocess sourcename preproname;
+      compile_i_file sourcename preproname
+    end
 
 let _ = print_endline "Hello world"
diff --git a/lib/CompCert b/lib/CompCert
index 849a9d2..636dec4 160000
--- a/lib/CompCert
+++ b/lib/CompCert
@@ -1 +1 @@
-Subproject commit 849a9d29216c17711ad00b8623016427d28efa09
+Subproject commit 636dec4c2dff5c58f7b46d01af896a5f17f6920a
-- 
cgit