diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-03-25 23:43:59 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-25 23:43:59 +0000 |
commit | 539177f4675398e72d59e03c04aa0ec907d7c08b (patch) | |
tree | fe224e2cd920b14c69c90d9763df479cd400f2ef /driver | |
parent | b71997d5928750f4ca2d8d749a99a49d33c61124 (diff) | |
download | vericert-539177f4675398e72d59e03c04aa0ec907d7c08b.tar.gz vericert-539177f4675398e72d59e03c04aa0ec907d7c08b.zip |
Move driver
Diffstat (limited to 'driver')
-rw-r--r-- | driver/CompCert.v | 97 | ||||
-rw-r--r-- | driver/Driver.ml | 19 | ||||
-rw-r--r-- | driver/dune | 9 |
3 files changed, 125 insertions, 0 deletions
diff --git a/driver/CompCert.v b/driver/CompCert.v new file mode 100644 index 0000000..d8dcb97 --- /dev/null +++ b/driver/CompCert.v @@ -0,0 +1,97 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +From compcert.common Require Import + Errors + Linking. + +From compcert.lib Require Import + Coqlib. + +From compcert.backend Require + Selection + RTL + RTLgen + Tailcall + Inlining + Renumber + Constprop + CSE + Deadcode + Unusedglob. + +From compcert.cfrontend Require + Csyntax + SimplExpr + SimplLocals + Cshmgen + Cminorgen. + +From compcert.driver Require + Compiler. + +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). + +Definition transf_frontend (p: Csyntax.program) : res RTL.program := + OK p + @@@ SimplExpr.transl_program + @@@ SimplLocals.transf_program + @@@ Cshmgen.transl_program + @@@ Cminorgen.transl_program + @@@ Selection.sel_program + @@@ RTLgen.transl_program. + +Local Open Scope linking_scope. + +Definition CompCert's_passes := + mkpass SimplExprproof.match_prog + ::: mkpass SimplLocalsproof.match_prog + ::: mkpass Cshmgenproof.match_prog + ::: mkpass Cminorgenproof.match_prog + ::: mkpass Selectionproof.match_prog + ::: mkpass RTLgenproof.match_prog + ::: pass_nil _. + +Definition match_prog: Csyntax.program -> RTL.program -> Prop := + pass_match (compose_passes CompCert's_passes). + +Theorem transf_frontend_match: + forall p tp, + transf_frontend p = OK tp -> + match_prog p tp. +Proof. + intros p tp T. + unfold transf_frontend in T. simpl in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. + 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. + 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. + exists p2; split. apply SimplLocalsproof.match_transf_program; auto. + exists p3; split. apply Cshmgenproof.transf_program_match; auto. + exists p4; split. apply Cminorgenproof.transf_program_match; auto. + exists p5; split. apply Selectionproof.transf_program_match; auto. + exists p6; split. apply RTLgenproof.transf_program_match; auto. + inversion T. reflexivity. +Qed. diff --git a/driver/Driver.ml b/driver/Driver.ml new file mode 100644 index 0000000..75ade9e --- /dev/null +++ b/driver/Driver.ml @@ -0,0 +1,19 @@ +(* + * CoqUp: Verified high-level synthesis. + * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com> + * + * This program is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * This program is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with this program. If not, see <https://www.gnu.org/licenses/>. + *) + +let _ = print_string (Coqup.PrettyPrint.prettyprint Coqup.VerilogAST.verilog_example) diff --git a/driver/dune b/driver/dune new file mode 100644 index 0000000..583f201 --- /dev/null +++ b/driver/dune @@ -0,0 +1,9 @@ +(include_subdirs no) + +(executables + (names Driver) + (libraries coqup)) + +(install + (section bin) + (files (Driver.exe as coqup))) |