aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-02-14 21:02:44 +0000
committerYann Herklotz <git@yannherklotz.com>2020-02-14 21:02:44 +0000
commitff40ff40ee967f6fd9206ef8c86426b0ea33cbde (patch)
tree81bfa37c75c73feb0131a2856c20ec81357222a2
parentc1f2c2e386c2597fdc61509ab2376f61f120c119 (diff)
downloadvericert-ff40ff40ee967f6fd9206ef8c86426b0ea33cbde.tar.gz
vericert-ff40ff40ee967f6fd9206ef8c86426b0ea33cbde.zip
Update driver
-rw-r--r--example/main.c9
-rw-r--r--example/main.v79
-rw-r--r--extraction/driver.ml66
m---------lib/CompCert0
4 files changed, 148 insertions, 6 deletions
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
-Subproject 849a9d29216c17711ad00b8623016427d28efa0
+Subproject 636dec4c2dff5c58f7b46d01af896a5f17f6920