diff options
| -rw-r--r-- | src/Compiler.v | 25 | ||||
| -rw-r--r-- | src/extraction/Extraction.v | 3 | ||||
| -rw-r--r-- | src/translation/Veriloggen.v | 38 |
3 files changed, 45 insertions, 21 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index a3a61a2..7a88839 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -50,17 +50,34 @@ From coqup Require Veriloggen HTLgen. +Parameter print_RTL: Z -> RTL.program -> unit. + +Definition print {A: Type} (printer: A -> unit) (prog: A) : A := + let unused := printer prog in prog. + +Lemma print_identity: + forall (A: Type) (printer: A -> unit) (prog: A), + print printer prog = prog. +Proof. + intros; unfold print. destruct (printer prog); auto. +Qed. + Notation "a @@@ b" := (Compiler.apply_partial _ _ a b) (at level 50, left associativity). Notation "a @@ b" := (Compiler.apply_total _ _ a b) (at level 50, left associativity). +Lemma compose_print_identity: + forall (A: Type) (x: res A) (f: A -> unit), + x @@ print f = x. +Proof. + intros. destruct x; simpl. rewrite print_identity. auto. auto. +Qed. + Definition transf_backend (r : RTL.program) : res Verilog.verilog := OK r - @@@ HTLgen.transf_program @@@ Veriloggen.transf_program. - Definition transf_frontend (p: Csyntax.program) : res RTL.program := OK p @@@ SimplExpr.transl_program @@ -68,7 +85,8 @@ Definition transf_frontend (p: Csyntax.program) : res RTL.program := @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ Selection.sel_program - @@@ RTLgen.transl_program. + @@@ RTLgen.transl_program + @@ print (print_RTL 0). Definition transf_hls (p : Csyntax.program) : res Verilog.verilog := OK p @@ -101,6 +119,7 @@ Proof. destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold match_prog; simpl. exists p1; split. apply SimplExprproof.transf_program_match; auto. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index e71721e..4403019 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -126,12 +126,15 @@ Extract Constant Compopts.debug => (* Compiler *) Extract Constant Compiler.print_Clight => "PrintClight.print_if". Extract Constant Compiler.print_Cminor => "PrintCminor.print_if". +Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_LTL => "PrintLTL.print_if". Extract Constant Compiler.print_Mach => "PrintMach.print_if". Extract Constant Compiler.print => "fun (f: 'a -> unit) (x: 'a) -> f x; x". Extract Constant Compiler.time => "Timing.time_coq". +Extract Constant Coquplib.debug_print => "print_newline". + (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) diff --git a/src/translation/Veriloggen.v b/src/translation/Veriloggen.v index c400617..605448b 100644 --- a/src/translation/Veriloggen.v +++ b/src/translation/Veriloggen.v @@ -18,9 +18,10 @@ From Coq Require Import FSets.FMapPositive. -From coqup Require Import HTL Verilog Coquplib. +From coqup Require Import Verilog Coquplib. From compcert Require Errors Op AST Integers. +From compcert Require Import RTL. Definition node : Type := positive. Definition reg : Type := positive. @@ -188,20 +189,21 @@ Definition option_err {A : Type} (str : string) (v : option A) (s : state) : mon Definition transf_instr (n : node) (i : instruction) (s : state) : mon node := match i with - | Hnop n' => + | Inop n' => add_instr n n' s Vskip - | Hnonblock op args dst n' => + | Iop op args dst n' => match translate_instr op args with | Some instr => add_instr n n' s (nonblock dst instr) | _ => Error (Errors.msg "Instruction is not implemented.") end - | Hload _ _ _ _ _ => Error (Errors.msg "Loads are not implemented.") - | Hstore _ _ _ _ _ => Error (Errors.msg "Stores are not implemented.") - | Hinst _ _ _ _ => Error (Errors.msg "Calls are not implemented.") - | Htailcall _ _ _ => Error (Errors.msg "Tailcalls are not implemented.") - | Hcond cond args n1 n2 => Error (Errors.msg "Condition not implemented.") - | Hjumptable _ _ => Error (Errors.msg "Jumptable not implemented.") - | Hfinish r => + | Iload _ _ _ _ _ => Error (Errors.msg "Loads are not implemented.") + | Istore _ _ _ _ _ => Error (Errors.msg "Stores are not implemented.") + | Icall _ _ _ _ _ => Error (Errors.msg "Calls are not implemented.") + | Itailcall _ _ _ => Error (Errors.msg "Tailcalls are not implemented.") + | Ibuiltin _ _ _ _ => Error (Errors.msg "Builtin functions not implemented.") + | Icond cond args n1 n2 => Error (Errors.msg "Condition not implemented.") + | Ijumptable _ _ => Error (Errors.msg "Jumptable not implemented.") + | Ireturn r => match r with | Some x => OK n s | None => OK n s @@ -232,25 +234,25 @@ Definition make_verilog (s : state) : verilog := (** To start out with, the assumption is made that there is only one function/module in the original code. *) -Definition transf_module (m: module) : Errors.res verilog := - match PTree.traverse transf_instr m.(mod_code) with +Definition transf_module (m: function) : Errors.res verilog := + match PTree.traverse transf_instr m.(fn_code) with | OK _ s => Errors.OK (make_verilog s) | Error err => Errors.Error err end. -Fixpoint main_module (main : ident) (flist : list (ident * AST.globdef moddecl unit)) - {struct flist} : option module := +Fixpoint main_function (main : ident) (flist : list (ident * AST.globdef fundef unit)) + {struct flist} : option function := match flist with | (i, AST.Gfun (AST.Internal f)) :: xs => if Pos.eqb i main then Some f - else main_module main xs - | _ :: xs => main_module main xs + else main_function main xs + | _ :: xs => main_function main xs | nil => None end. -Definition transf_program (d : design) : Errors.res verilog := - match main_module d.(AST.prog_main) d.(AST.prog_defs) with +Definition transf_program (d : program) : Errors.res verilog := + match main_function d.(AST.prog_main) d.(AST.prog_defs) with | Some m => transf_module m | _ => Errors.Error (Errors.msg "Could not find main module") end. |