From 539177f4675398e72d59e03c04aa0ec907d7c08b Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 25 Mar 2020 23:43:59 +0000 Subject: Move driver --- src/driver/CompCert.v | 97 --------------------------------------------------- src/driver/Driver.ml | 22 ------------ src/driver/dune | 7 ---- 3 files changed, 126 deletions(-) delete mode 100644 src/driver/CompCert.v delete mode 100644 src/driver/Driver.ml delete mode 100644 src/driver/dune (limited to 'src') diff --git a/src/driver/CompCert.v b/src/driver/CompCert.v deleted file mode 100644 index d8dcb97..0000000 --- a/src/driver/CompCert.v +++ /dev/null @@ -1,97 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -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/src/driver/Driver.ml b/src/driver/Driver.ml deleted file mode 100644 index 40a45e6..0000000 --- a/src/driver/Driver.ml +++ /dev/null @@ -1,22 +0,0 @@ -(* - * CoqUp: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 . - *) - -open Verilog -open Extraction - -let _ = print_string (PrettyPrint.prettyprint VerilogAST.verilog_example) diff --git a/src/driver/dune b/src/driver/dune deleted file mode 100644 index e295a76..0000000 --- a/src/driver/dune +++ /dev/null @@ -1,7 +0,0 @@ -(executables - (names Driver) - (libraries compcert coqup.verilog coqup.extraction)) - -(install - (section bin) - (files (Driver.exe as coqup))) -- cgit