diff options
43 files changed, 4239 insertions, 811 deletions
@@ -62,3 +62,71 @@ lib/COMPCERTSTAMP # Misc lpsolve.txt + +# Benchmarks + +benchmarks/**/*.v + +*.gcc +*.iver +*.dot + +/benchmarks/polybench-syn/stencils/seidel-2d +/benchmarks/polybench-syn/stencils/jacobi-2d +/benchmarks/polybench-syn/data-mining/covariance +/benchmarks/polybench-syn/linear-algebra/blas/gemm +/benchmarks/polybench-syn/linear-algebra/blas/gemver +/benchmarks/polybench-syn/linear-algebra/blas/gesummv +/benchmarks/polybench-syn/linear-algebra/blas/symm +/benchmarks/polybench-syn/linear-algebra/blas/syr2k +/benchmarks/polybench-syn/linear-algebra/blas/syrk +/benchmarks/polybench-syn/linear-algebra/blas/trmm +/benchmarks/polybench-syn/linear-algebra/kernels/2mm +/benchmarks/polybench-syn/linear-algebra/kernels/3mm +/benchmarks/polybench-syn/linear-algebra/kernels/atas +/benchmarks/polybench-syn/linear-algebra/kernels/bicg +/benchmarks/polybench-syn/linear-algebra/kernels/doitgen +/benchmarks/polybench-syn/linear-algebra/kernels/mvt +/benchmarks/polybench-syn/linear-algebra/solvers/cholesky +/benchmarks/polybench-syn/linear-algebra/solvers/durbin +/benchmarks/polybench-syn/linear-algebra/solvers/lu +/benchmarks/polybench-syn/linear-algebra/solvers/ludcmp +/benchmarks/polybench-syn/linear-algebra/solvers/trisolv +/benchmarks/polybench-syn/medley/floyd-warshall +/benchmarks/polybench-syn/medley/nussinov +/benchmarks/polybench-syn/stencils/adi +/benchmarks/polybench-syn/stencils/fdtd-2d +/benchmarks/polybench-syn/stencils/heat-3d +/benchmarks/polybench-syn/stencils/jacobi-1d + +/benchmarks/polybench-syn-div/stencils/seidel-2d +/benchmarks/polybench-syn-div/stencils/jacobi-2d +/benchmarks/polybench-syn-div/data-mining/covariance +/benchmarks/polybench-syn-div/linear-algebra/blas/gemm +/benchmarks/polybench-syn-div/linear-algebra/blas/gemver +/benchmarks/polybench-syn-div/linear-algebra/blas/gesummv +/benchmarks/polybench-syn-div/linear-algebra/blas/symm +/benchmarks/polybench-syn-div/linear-algebra/blas/syr2k +/benchmarks/polybench-syn-div/linear-algebra/blas/syrk +/benchmarks/polybench-syn-div/linear-algebra/blas/trmm +/benchmarks/polybench-syn-div/linear-algebra/kernels/2mm +/benchmarks/polybench-syn-div/linear-algebra/kernels/3mm +/benchmarks/polybench-syn-div/linear-algebra/kernels/atas +/benchmarks/polybench-syn-div/linear-algebra/kernels/bicg +/benchmarks/polybench-syn-div/linear-algebra/kernels/doitgen +/benchmarks/polybench-syn-div/linear-algebra/kernels/mvt +/benchmarks/polybench-syn-div/linear-algebra/solvers/cholesky +/benchmarks/polybench-syn-div/linear-algebra/solvers/durbin +/benchmarks/polybench-syn-div/linear-algebra/solvers/lu +/benchmarks/polybench-syn-div/linear-algebra/solvers/ludcmp +/benchmarks/polybench-syn-div/linear-algebra/solvers/trisolv +/benchmarks/polybench-syn-div/medley/floyd-warshall +/benchmarks/polybench-syn-div/medley/nussinov +/benchmarks/polybench-syn-div/stencils/adi +/benchmarks/polybench-syn-div/stencils/fdtd-2d +/benchmarks/polybench-syn-div/stencils/heat-3d +/benchmarks/polybench-syn-div/stencils/jacobi-1d + +# Test +*.check +*.txt diff --git a/CHANGELOG.org b/CHANGELOG.org index 621683c..88c0953 100644 --- a/CHANGELOG.org +++ b/CHANGELOG.org @@ -1,42 +1,65 @@ # -*- fill-column: 80 -*- +#+title: Vericert Changelog +#+author: Yann Herklotz +#+email: git@ymhg.org -* Vericert Changelog +* Unreleased -** Unreleased +** New Features -*** New Features - -- Add *RTLBlock*, a basic block intermediate language that is based on CompCert's +- Add ~RTLBlock~, a basic block intermediate language that is based on CompCert's RTL. -- Add *RTLPar*, which can execute groups of instructions in parallel. -- Add scheduling pass to go from RTLBlock to RTLPar. +- Add ~RTLPar~, which can execute groups of instructions in parallel. +- Add SDC hyper-block scheduling pass to go from RTLBlock to RTLPar using. +- Add operation chaining support to scheduler. +- Add ~Abstr~ intermediate language for equivalence checking of schedule. +- Add built-in verified SAT solver used for equivalence checking of + hyper-blocks. + +* 2021-10-01 - v1.2.2 + +Mainly fix some documentation and remove any ~Admitted~ theorems, even though +these were in parts of the compiler that were never used. + +* 2021-07-12 - v1.2.1 + +Main release for OOPSLA'21 paper. + +- Add better documentation on how to run Vericert. +- Add =Dockerfile= with instructions on how to get figures of the paper. + +* 2021-04-07 - v1.2.0 + +** New Features + +- Add memory inference capabilities in generated hardware. -** v1.1.0 - 2020-12-17 +* 2020-12-17 - v1.1.0 Add a stable release with all proofs completed. -** v1.0.1 - 2020-08-14 +* 2020-08-14 - v1.0.1 Release a new minor version fixing all proofs and fixing scripts to generate the badges. -*** Bug Fixes +** Fixes - Fix some of the proofs which were not passing. -** v1.0.0 - 2020-08-13 +* 2020-08-13 - v1.0.0 First release of a fully verified version of Vericert with support for the translation of many C constructs to Verilog. -*** New Features +** New Features - Most int instructions and operators. - Non-recursive function calls. - Local arrays, structs and unions of type int. - Pointer arithmetic with int. -** v0.1.0 - 2020-04-03 +* 2020-04-03 - v0.1.0 This is the first release with working HLS but without any proofs associated with it. diff --git a/CITATION.cff b/CITATION.cff index 9328474..c114ec6 100644 --- a/CITATION.cff +++ b/CITATION.cff @@ -15,9 +15,9 @@ authors: given-names: "John" orcid: "https://orcid.org/0000-0001-6735-5533" title: "Vericert" -version: 1.2.1 +version: 1.2.2 doi: 10.5281/zenodo.5093839 -date-released: 2021-07-12 +date-released: 2021-10-01 url: "https://github.com/ymherklotz/vericert" preferred-citation: type: article @@ -54,7 +54,7 @@ doc: Makefile.coq extraction: src/extraction/STAMP test: - ./test/test_all.sh ./test + $(MAKE) -C test compile: src/extraction/STAMP @echo "OCaml bin/vericert" @@ -73,6 +73,7 @@ Makefile.coq: clean:: Makefile.coq $(MAKE) -f Makefile.coq clean + $(MAKE) -C test clean rm -f Makefile.coq clean:: @@ -1,3 +1,5 @@ +#+title: + #+html: <a href="https://vericert.ymhg.org"><img src="https://vericert.ymhg.org/vericert-main.svg" width="100%" height="144" /></a> #+html: <p align=center><a href="https://github.com/ymherklotz/vericert/actions"><img src="https://github.com/ymherklotz/vericert/workflows/CI/badge.svg" /></a> <a href="https://vericert.ymhg.org/"><img src="https://github.com/ymherklotz/vericert-docs/workflows/docs/badge.svg" /></a></p> @@ -11,8 +13,8 @@ correctness. :PROPERTIES: :CUSTOM_ID: features :END: -The project is currently a work in progress, so proofs remain to be finished. Currently, the -following C features are supported, but are not all proven correct yet: + +Currently all proofs of the following features have been completed. - all int operations, - non-recursive function calls, @@ -32,7 +34,6 @@ compiled and executed. The dependencies of this project are the following: - [[https://coq.inria.fr/][Coq]]: theorem prover that is used to also program the HLS tool. - [[https://ocaml.org/][OCaml]]: the OCaml compiler to compile the extracted files. -- [[https://github.com/mit-plv/bbv][bbv]]: an efficient bit vector library. - [[https://github.com/ocaml/dune][dune]]: build tool for ocaml projects to gather all the ocaml files and compile them in the right order. - [[http://gallium.inria.fr/~fpottier/menhir/][menhir]]: parser generator for ocaml. @@ -41,23 +42,25 @@ compiled and executed. The dependencies of this project are the following: These dependencies can be installed manually, or automatically through Nix. -*** Downloading CompCert +*** Downloading Vericert and CompCert :PROPERTIES: :CUSTOM_ID: downloading-compcert :END: CompCert is added as a submodule in the =lib/CompCert= directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded -together with the repository. To clone CompCert together with this project, you can run: +together with the repository. To clone CompCert together with this project, and check it out at the +correct revision, you can run: #+begin_src shell - git clone --recursive https://github.com/ymherklotz/vericert +git clone -b v1.2.2 --recursive https://github.com/ymherklotz/vericert #+end_src If the repository is already cloned, you can run the following command to make sure that CompCert is -also downloaded: +also downloaded and the correct branch is checked out: #+begin_src shell - git submodule update --init +git checkout v1.2.2 +git submodule update --init #+end_src *** Setting up Nix @@ -70,7 +73,7 @@ reproducible. Once nix is installed, it can be used in the following way. To open a shell which includes all the necessary dependencies, one can use: #+begin_src shell - nix-shell +nix-shell #+end_src which will open a shell that has all the dependencies loaded. @@ -83,7 +86,7 @@ If the dependencies were installed manually, or if one is in the =nix-shell=, th by running: #+begin_src shell - make -j8 +make -j8 #+end_src and installed locally, or under the =PREFIX= location using: @@ -103,9 +106,9 @@ To test out =vericert= you can try the following examples which are in the test following: #+begin_src shell - ./bin/vericert test/loop.c -o loop.v - ./bin/vericert test/conditional.c -o conditional.v - ./bin/vericert test/add.c -o add.v +./bin/vericert test/loop.c -o loop.v +./bin/vericert test/conditional.c -o conditional.v +./bin/vericert test/add.c -o add.v #+end_src ** Citation diff --git a/benchmarks/polybench-syn/common.mk b/benchmarks/polybench-syn/common.mk index fbada0b..4c6374f 100644 --- a/benchmarks/polybench-syn/common.mk +++ b/benchmarks/polybench-syn/common.mk @@ -1,5 +1,5 @@ VERICERT ?= vericert -VERICERT_OPTS ?= -DSYNTHESIS +VERICERT_OPTS ?= -DSYNTHESIS -fschedule IVERILOG ?= iverilog IVERILOG_OPTS ?= diff --git a/default.nix b/default.nix index 762d38b..0125fdd 100644 --- a/default.nix +++ b/default.nix @@ -1,4 +1,4 @@ -with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/8dd8bd8be74879f9f7919b16a4cb5ab2a75f18e5.tar.gz") {}; +with import (fetchTarball "https://github.com/NixOS/nixpkgs/archive/1a56d76d718afb6c47dd96602c915b6d23f7c45d.tar.gz") {}; let ncoq = coq_8_13; ncoqPackages = coqPackages_8_13; @@ -9,7 +9,13 @@ stdenv.mkDerivation { buildInputs = [ ncoq ncoqPackages.coqhammer cvc4 eprover z3-tptp dune_2 gcc ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir - ncoq.ocamlPackages.ocamlgraph + ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin + ncoq.ocamlPackages.menhirLib + + ncoqPackages.serapi + python3 python3Packages.docutils python3Packages.pygments + python3Packages.dominate + python3Packages.pelican ]; enableParallelBuilding = true; diff --git a/docs b/docs -Subproject 3b2ce146bc6e651df8ac9910d08da05d88c06fb +Subproject 20ed00b92c1a5bf2806a27e9c85d90c6d265e5b diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 1ea580f..a36f375 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -65,6 +65,8 @@ let compile_c_file sourcename ifile ofile = set_dest Vericert.PrintClight.destination option_dclight ".light.c"; set_dest Vericert.PrintCminor.destination option_dcminor ".cm"; set_dest Vericert.PrintRTL.destination option_drtl ".rtl"; + set_dest Vericert.PrintRTLBlock.destination option_drtlblock ".rtlblock"; + set_dest Vericert.PrintRTLPar.destination option_drtlpar ".rtlpar"; set_dest Vericert.PrintHTL.destination option_dhtl ".htl"; set_dest Vericert.Regalloc.destination_alloctrace option_dalloctrace ".alloctrace"; set_dest Vericert.PrintLTL.destination option_dltl ".ltl"; @@ -92,7 +94,7 @@ let compile_c_file sourcename ifile ofile = end else begin let verilog = let translation = if !option_hls_schedule - then Vericert.Compiler0.transf_hls + then Vericert.Compiler0.transf_hls_temp else Vericert.Compiler0.transf_hls in match translation csyntax with @@ -390,6 +392,7 @@ let cmdline_actions = Exact "-dcminor", Set option_dcminor; Exact "-drtl", Set option_drtl; Exact "-drtlblock", Set option_drtlblock; + Exact "-drtlpar", Set option_drtlpar; Exact "-dhtl", Set option_dhtl; Exact "-dltl", Set option_dltl; Exact "-dalloctrace", Set option_dalloctrace; @@ -403,6 +406,7 @@ let cmdline_actions = option_dcminor := true; option_drtl := true; option_drtlblock := true; + option_drtlpar := true; option_dhtl := true; option_dltl := true; option_dalloctrace := true; diff --git a/src/Compiler.v b/src/Compiler.v index bb9575e..1b615d2 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -85,6 +85,7 @@ We then need to declare the external OCaml functions used to print out intermedi Parameter print_RTL: Z -> RTL.program -> unit. Parameter print_HTL: Z -> HTL.program -> unit. Parameter print_RTLBlock: Z -> RTLBlock.program -> unit. +Parameter print_RTLPar: Z -> RTLPar.program -> unit. Definition print {A: Type} (printer: A -> unit) (prog: A) : A := let unused := printer prog in prog. @@ -223,7 +224,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := (* This is an unverified version of transf_hls with some experimental additions such as scheduling that aren't completed yet. *) -(*Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := +Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program := OK p @@@ SimplExpr.transl_program @@@ SimplLocals.transf_program @@ -246,13 +247,14 @@ that aren't completed yet. *) @@@ time "Unused globals" Unusedglob.transform_program @@ print (print_RTL 7) @@@ RTLBlockgen.transl_program - @@ print (print_RTLBlock 1) + @@ print (print_RTLBlock 0) @@ total_if HLSOpts.optim_if_conversion IfConversion.transf_program - @@ print (print_RTLBlock 2) + @@ print (print_RTLBlock 1) @@@ RTLPargen.transl_program + @@ print (print_RTLPar 0) @@@ HTLPargen.transl_program - @@ print print_HTL - @@ Veriloggen.transl_program.*) + @@ print (print_HTL 0) + @@ Veriloggen.transl_program. (*| Correctness Proof diff --git a/src/VericertClflags.ml b/src/VericertClflags.ml index 977ca00..ab3c949 100644 --- a/src/VericertClflags.ml +++ b/src/VericertClflags.ml @@ -5,6 +5,7 @@ let option_debug_hls = ref false let option_initial = ref false let option_dhtl = ref false let option_drtlblock = ref false +let option_drtlpar = ref false let option_hls_schedule = ref false let option_fif_conv = ref false let option_fram = ref true diff --git a/src/common/Monad.v b/src/common/Monad.v index c9cdc1a..1801a63 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -42,10 +42,10 @@ Module MonadExtra(M : Monad). Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). + (at level 200, X name, A at level 100, B at level 200). Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B)) - (at level 200, X ident, Y ident, A at level 100, B at level 200). + (at level 200, X name, Y name, A at level 100, B at level 200). End MonadNotation. Import MonadNotation. diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index 805dbda..331e015 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -34,7 +34,7 @@ Require Import vericert.common.Show. (* Depend on CompCert for the basic library, as they declare and prove some useful theorems. *) -Local Open Scope Z_scope. +#[local] Open Scope Z_scope. (* This tactic due to Clement Pit-Claudel with some minor additions by JDP to allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) @@ -235,8 +235,8 @@ Ltac crush_trans := Ltac maybe t := t + idtac. -Global Opaque Nat.div. -Global Opaque Z.mul. +#[global] Opaque Nat.div. +#[global] Opaque Z.mul. Inductive Ascending : list positive -> Prop := | Ascending_nil : Ascending nil @@ -320,7 +320,7 @@ Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B := Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). + (at level 200, X name, A at level 100, B at level 200). End Notation. End Option. diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v index 6abe4e0..97f0d2a 100644 --- a/src/extraction/Extraction.v +++ b/src/extraction/Extraction.v @@ -144,6 +144,7 @@ Extract Constant driver.Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTL => "PrintRTL.print_if". Extract Constant Compiler.print_RTLBlock => "PrintRTLBlock.print_if". Extract Constant Compiler.print_HTL => "PrintHTL.print_if". +Extract Constant Compiler.print_RTLPar => "PrintRTLPar.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". @@ -179,7 +180,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". Extract Constant Pipeline.pipeline => "SoftwarePipelining.pipeline". Extract Constant RTLBlockgen.partition => "Partition.partition". -(*Extract Constant RTLPargen.schedule => "Schedule.schedule_fn".*) +Extract Constant RTLPargen.schedule => "Schedule.schedule_fn". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. @@ -187,11 +188,11 @@ Set Extraction AccessOpaque. Cd "src/extraction". Separate Extraction Verilog.module vericert.Compiler.transf_hls -(* vericert.Compiler.transf_hls_temp*) -(* RTLBlockgen.transl_program RTLBlockInstr.successors_instr*) + vericert.Compiler.transf_hls_temp + RTLBlockgen.transl_program RTLBlockInstr.successors_instr HTLgen.tbl_to_case_expr Pipeline.pipeline -(* RTLBlockInstr.sat_pred_temp*) + RTLBlockInstr.sat_pred_simple Verilog.stmnt_to_list Compiler.transf_c_program Compiler.transf_cminor_program diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v new file mode 100644 index 0000000..54a6c07 --- /dev/null +++ b/src/hls/Abstr.v @@ -0,0 +1,973 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 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/>. + *) + +Require Import compcert.backend.Registers. +Require Import compcert.common.AST. +Require Import compcert.common.Globalenvs. +Require Import compcert.common.Memory. +Require Import compcert.common.Values. +Require Import compcert.lib.Floats. +Require Import compcert.lib.Integers. +Require Import compcert.lib.Maps. +Require compcert.verilog.Op. + +Require Import vericert.common.Vericertlib. +Require Import vericert.hls.RTLBlock. +Require Import vericert.hls.RTLPar. +Require Import vericert.hls.RTLBlockInstr. +Require Import vericert.hls.HashTree. + +#[local] Open Scope positive. +#[local] Open Scope pred_op. + +(*| +Schedule Oracle +=============== + +This oracle determines if a schedule was valid by performing symbolic execution on the input and +output and showing that these behave the same. This acts on each basic block separately, as the +rest of the functions should be equivalent. +|*) + +Definition reg := positive. + +Inductive resource : Set := +| Reg : reg -> resource +| Pred : reg -> resource +| Mem : resource. + +(*| +The following defines quite a few equality comparisons automatically, however, these can be +optimised heavily if written manually, as their proofs are not needed. +|*) + +Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}. +Proof. + decide equality; apply Pos.eq_dec. +Defined. + +Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. +Proof. + generalize comparison_eq; intro. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + decide equality. +Defined. + +Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. +Proof. + generalize Int.eq_dec; intro. + generalize AST.ident_eq; intro. + generalize Z.eq_dec; intro. + generalize Ptrofs.eq_dec; intro. + decide equality. +Defined. + +Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. +Proof. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. + generalize AST.ident_eq; intro. + generalize condition_eq; intro. + generalize addressing_eq; intro. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. +Proof. + decide equality. +Defined. + +Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. +Proof. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. +Proof. + generalize typ_eq; intro. + decide equality. +Defined. + +Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Defined. + +Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. +Proof. + generalize operation_eq; intro. + decide equality. +Defined. + +Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intros. + decide equality. +Defined. + +Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. +Proof. + repeat decide equality. +Defined. + +Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intro. + generalize typ_eq; intro. + generalize Int.eq_dec; intro. + generalize memory_chunk_eq; intro. + generalize addressing_eq; intro. + generalize operation_eq; intro. + generalize condition_eq; intro. + generalize signature_eq; intro. + generalize list_operation_eq; intro. + generalize list_reg_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. +Proof. + generalize Pos.eq_dec; intro. + generalize typ_eq; intro. + generalize Int.eq_dec; intro. + generalize Int64.eq_dec; intro. + generalize Float.eq_dec; intro. + generalize Float32.eq_dec; intro. + generalize Ptrofs.eq_dec; intro. + generalize memory_chunk_eq; intro. + generalize addressing_eq; intro. + generalize operation_eq; intro. + generalize condition_eq; intro. + generalize signature_eq; intro. + generalize list_operation_eq; intro. + generalize list_reg_eq; intro. + generalize AST.ident_eq; intro. + repeat decide equality. +Defined. + +(*| +We then create equality lemmas for a resource and a module to index resources uniquely. The +indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be +shifted right by 1. This means that they will never overlap. +|*) + +Module R_indexed. + Definition t := resource. + Definition index (rs: resource) : positive := + match rs with + | Reg r => xO (xO r) + | Pred r => xI (xI r) + | Mem => 1%positive + end. + + Lemma index_inj: forall (x y: t), index x = index y -> x = y. + Proof. destruct x; destruct y; crush. Qed. + + Definition eq := resource_eq. +End R_indexed. + +(*| +We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use +expressions instead of registers as their inputs and outputs. This means that we can accumulate all +the results of the operations as general expressions that will be present in those registers. + +- Ebase: the starting value of the register. +- Eop: Some arithmetic operation on a number of registers. +- Eload: A load from a memory location into a register. +- Estore: A store from a register to a memory location. + +Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as +that enables mutual recursive definitions over the datatypes. +|*) + +Definition unsat p := forall a, sat_predicate p a = false. +Definition sat p := exists a, sat_predicate p a = true. + +Inductive expression : Type := +| Ebase : resource -> expression +| Eop : Op.operation -> expression_list -> expression +| Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression +| Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression +| Esetpred : Op.condition -> expression_list -> expression +with expression_list : Type := +| Enil : expression_list +| Econs : expression -> expression_list -> expression_list +. + +(*Inductive pred_expr : Type := +| PEsingleton : option pred_op -> expression -> pred_expr +| PEcons : option pred_op -> expression -> pred_expr -> pred_expr.*) + +Module NonEmpty. + +Inductive non_empty (A: Type) := +| singleton : A -> non_empty A +| cons : A -> non_empty A -> non_empty A +. + +Arguments singleton [A]. +Arguments cons [A]. + +Declare Scope non_empty_scope. +Delimit Scope non_empty_scope with non_empty. + +Module NonEmptyNotation. +Infix "::|" := cons (at level 60, right associativity) : non_empty_scope. +End NonEmptyNotation. +Import NonEmptyNotation. + +#[local] Open Scope non_empty_scope. + +Fixpoint map {A B} (f: A -> B) (l: non_empty A): non_empty B := + match l with + | singleton a => singleton (f a) + | a ::| b => f a ::| map f b + end. + +Fixpoint to_list {A} (l: non_empty A): list A := + match l with + | singleton a => a::nil + | a ::| b => a :: to_list b + end. + +Fixpoint app {A} (l1 l2: non_empty A) := + match l1 with + | singleton a => a ::| l2 + | a ::| b => a ::| app b l2 + end. + +Fixpoint non_empty_prod {A B} (l: non_empty A) (l': non_empty B) := + match l with + | singleton a => map (fun x => (a, x)) l' + | a ::| b => app (map (fun x => (a, x)) l') (non_empty_prod b l') + end. + +Fixpoint of_list {A} (l: list A): option (non_empty A) := + match l with + | a::b => + match of_list b with + | Some b' => Some (a ::| b') + | _ => None + end + | nil => None + end. + +Inductive In {A: Type} (x: A) : non_empty A -> Prop := +| In_cons : forall a b, x = a \/ In x b -> In x (a ::| b) +| In_single : In x (singleton x). + +End NonEmpty. + +Module NE := NonEmpty. +Import NE.NonEmptyNotation. + +#[local] Open Scope non_empty_scope. + +Definition predicated_ne A := NE.non_empty (pred_op * A). + +Variant predicated A := +| Psingle : A -> predicated A +| Plist : predicated_ne A -> predicated A. + +Arguments Psingle [A]. +Arguments Plist [A]. + +Definition pred_expr_ne := predicated_ne expression. +Definition pred_expr := predicated expression. + +Inductive predicated_wf A : predicated A -> Prop := +| Psingle_wf : + forall a, predicated_wf A (Psingle a) +| Plist_wf : + forall a b l, + In a (map fst (NE.to_list l)) -> + In b (map fst (NE.to_list l)) -> + a <> b -> + unsat (Pand a b) -> + predicated_wf A (Plist l) +. + +(*| +Using IMap we can create a map from resources to any other type, as resources can be uniquely +identified as positive numbers. +|*) + +Module Rtree := ITree(R_indexed). + +Definition forest : Type := Rtree.t pred_expr. + +Definition get_forest v (f: forest) := + match Rtree.get v f with + | None => Psingle (Ebase v) + | Some v' => v' + end. + +Declare Scope forest. + +Notation "a # b" := (get_forest b a) (at level 1) : forest. +Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level) : forest. + +#[local] Open Scope forest. + +Definition maybe {A: Type} (vo: A) (pr: predset) p (v: A) := + match p with + | Some p' => if eval_predf pr p' then v else vo + | None => v + end. + +Definition get_pr i := match i with mk_instr_state a b c => b end. + +Definition get_m i := match i with mk_instr_state a b c => c end. + +Definition eval_predf_opt pr p := + match p with Some p' => eval_predf pr p' | None => true end. + +(*| +Finally we want to define the semantics of execution for the expressions with symbolic values, so +the result of executing the expressions will be an expressions. +|*) + +Section SEMANTICS. + +Context {A : Type}. + +Record ctx : Type := mk_ctx { + ctx_rs: regset; + ctx_ps: predset; + ctx_mem: mem; + ctx_sp: val; + ctx_ge: Genv.t A unit; +}. + +Inductive sem_value : ctx -> expression -> val -> Prop := +| Sbase_reg: + forall r ctx, + sem_value ctx (Ebase (Reg r)) ((ctx_rs ctx) !! r) +| Sop: + forall ctx op args v lv, + sem_val_list ctx args lv -> + Op.eval_operation (ctx_ge ctx) (ctx_sp ctx) op lv (ctx_mem ctx) = Some v -> + sem_value ctx (Eop op args) v +| Sload : + forall ctx mexp addr chunk args a v m' lv, + sem_mem ctx mexp m' -> + sem_val_list ctx args lv -> + Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a -> + Memory.Mem.loadv chunk m' a = Some v -> + sem_value ctx (Eload chunk addr args mexp) v +with sem_pred : ctx -> expression -> bool -> Prop := +| Spred: + forall ctx args c lv v, + sem_val_list ctx args lv -> + Op.eval_condition c lv (ctx_mem ctx) = Some v -> + sem_pred ctx (Esetpred c args) v +| Sbase_pred: + forall ctx p, + sem_pred ctx (Ebase (Pred p)) ((ctx_ps ctx) !! p) +with sem_mem : ctx -> expression -> Memory.mem -> Prop := +| Sstore : + forall ctx mexp vexp chunk addr args lv v a m' m'', + sem_mem ctx mexp m' -> + sem_value ctx vexp v -> + sem_val_list ctx args lv -> + Op.eval_addressing (ctx_ge ctx) (ctx_sp ctx) addr lv = Some a -> + Memory.Mem.storev chunk m' a v = Some m'' -> + sem_mem ctx (Estore vexp chunk addr args mexp) m'' +| Sbase_mem : + forall ctx, + sem_mem ctx (Ebase Mem) (ctx_mem ctx) +with sem_val_list : ctx -> expression_list -> list val -> Prop := +| Snil : + forall ctx, + sem_val_list ctx Enil nil +| Scons : + forall ctx e v l lv, + sem_value ctx e v -> + sem_val_list ctx l lv -> + sem_val_list ctx (Econs e l) (v :: lv) +. + +Inductive sem_pred_expr {B: Type} (sem: ctx -> expression -> B -> Prop): + ctx -> pred_expr -> B -> Prop := +| sem_pred_expr_base : + forall ctx e v, + sem ctx e v -> + sem_pred_expr sem ctx (Psingle e) v +| sem_pred_expr_cons_true : + forall ctx e pr p' v, + eval_predf (ctx_ps ctx) pr = true -> + sem ctx e v -> + sem_pred_expr sem ctx (Plist ((pr, e) ::| p')) v +| sem_pred_expr_cons_false : + forall ctx e pr p' v, + eval_predf (ctx_ps ctx) pr = false -> + sem_pred_expr sem ctx (Plist p') v -> + sem_pred_expr sem ctx (Plist ((pr, e) ::| p')) v +| sem_pred_expr_single : + forall ctx e pr v, + eval_predf (ctx_ps ctx) pr = true -> + sem_pred_expr sem ctx (Plist (NE.singleton (pr, e))) v +. + +Definition collapse_pe (p: pred_expr) : option expression := + match p with + | Psingle p => Some p + | _ => None + end. + +Inductive sem_predset : ctx -> forest -> predset -> Prop := +| Spredset: + forall ctx f rs', + (forall pe x, + collapse_pe (f # (Pred x)) = Some pe -> + sem_pred ctx pe (rs' !! x)) -> + sem_predset ctx f rs'. + +Inductive sem_regset : ctx -> forest -> regset -> Prop := +| Sregset: + forall ctx f rs', + (forall x, sem_pred_expr sem_value ctx (f # (Reg x)) (rs' !! x)) -> + sem_regset ctx f rs'. + +Inductive sem : ctx -> forest -> instr_state -> Prop := +| Sem: + forall ctx rs' m' f pr', + sem_regset ctx f rs' -> + sem_predset ctx f pr' -> + sem_pred_expr sem_mem ctx (f # Mem) m' -> + sem ctx f (mk_instr_state rs' pr' m'). + +End SEMANTICS. + +Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := + match e1, e2 with + | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false + | Eop op1 el1, Eop op2 el2 => + if operation_eq op1 op2 then + beq_expression_list el1 el2 else false + | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => + if memory_chunk_eq chk1 chk2 + then if addressing_eq addr1 addr2 + then if beq_expression_list el1 el2 + then beq_expression e1 e2 else false else false else false + | Estore e1 chk1 addr1 el1 m1, Estore e2 chk2 addr2 el2 m2 => + if memory_chunk_eq chk1 chk2 + then if addressing_eq addr1 addr2 + then if beq_expression_list el1 el2 + then if beq_expression m1 m2 + then beq_expression e1 e2 else false else false else false else false + | Esetpred c1 el1, Esetpred c2 el2 => + if condition_eq c1 c2 + then beq_expression_list el1 el2 else false + | _, _ => false + end +with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := + match el1, el2 with + | Enil, Enil => true + | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 + | _, _ => false + end +. + +Scheme expression_ind2 := Induction for expression Sort Prop + with expression_list_ind2 := Induction for expression_list Sort Prop. + +Lemma beq_expression_correct: + forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. +Proof. + intro e1; + apply expression_ind2 with + (P := fun (e1 : expression) => + forall e2, beq_expression e1 e2 = true -> e1 = e2) + (P0 := fun (e1 : expression_list) => + forall e2, beq_expression_list e1 e2 = true -> e1 = e2); simplify; + try solve [repeat match goal with + | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? + | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? + end; subst; f_equal; crush; eauto using Peqb_true_eq]. +Qed. + +Lemma beq_expression_refl: forall e, beq_expression e e = true. +Proof. + intros. + induction e using expression_ind2 with (P0 := fun el => beq_expression_list el el = true); + crush; repeat (destruct_match; crush); []. + crush. rewrite IHe. rewrite IHe0. auto. +Qed. + +Lemma beq_expression_list_refl: forall e, beq_expression_list e e = true. +Proof. induction e; auto. simplify. rewrite beq_expression_refl. auto. Qed. + +Lemma beq_expression_correct2: + forall e1 e2, beq_expression e1 e2 = false -> e1 <> e2. +Proof. + induction e1 using expression_ind2 + with (P0 := fun el1 => forall el2, beq_expression_list el1 el2 = false -> el1 <> el2). + - intros. simplify. repeat (destruct_match; crush). + - intros. simplify. repeat (destruct_match; crush). subst. apply IHe1 in H. + unfold not in *. intros. apply H. inv H0. auto. + - intros. simplify. repeat (destruct_match; crush); subst. + unfold not in *; intros. inv H0. rewrite beq_expression_refl in H. + discriminate. + unfold not in *; intros. inv H. rewrite beq_expression_list_refl in Heqb. discriminate. + - simplify. repeat (destruct_match; crush); subst; + unfold not in *; intros. + inv H0. rewrite beq_expression_refl in H; crush. + inv H. rewrite beq_expression_refl in Heqb0; crush. + inv H. rewrite beq_expression_list_refl in Heqb; crush. + - simplify. repeat (destruct_match; crush); subst. + unfold not in *; intros. inv H0. rewrite beq_expression_list_refl in H; crush. + - simplify. repeat (destruct_match; crush); subst. + - simplify. repeat (destruct_match; crush); subst. + apply andb_false_iff in H. inv H. unfold not in *; intros. + inv H. rewrite beq_expression_refl in H0; discriminate. + unfold not in *; intros. inv H. rewrite beq_expression_list_refl in H0; discriminate. +Qed. + +Lemma expression_dec: forall e1 e2: expression, {e1 = e2} + {e1 <> e2}. +Proof. + intros. + destruct (beq_expression e1 e2) eqn:?. apply beq_expression_correct in Heqb. auto. + apply beq_expression_correct2 in Heqb. auto. +Defined. + +Module HashExpr <: Hashable. + Definition t := expression. + Definition eq_dec := expression_dec. +End HashExpr. + +Module HT := HashTree(HashExpr). +Import HT. + +Definition combine_option {A} (a b: option A) : option A := + match a, b with + | Some a', _ => Some a' + | _, Some b' => Some b' + | _, _ => None + end. + +Fixpoint norm_expression_ne (max: predicate) (pe: pred_expr_ne) (h: hash_tree) + : (PTree.t pred_op) * hash_tree := + match pe with + | NE.singleton (p, e) => + let (p', h') := hash_value max e h in + (PTree.set p' p (PTree.empty _), h') + | (p, e) ::| pr => + let (p', h') := hash_value max e h in + let (p'', h'') := norm_expression_ne max pr h' in + match p'' ! p' with + | Some pr_op => + (PTree.set p' (pr_op ∨ p) p'', h'') + | None => + (PTree.set p' p p'', h'') + end + end. + +Definition encode_expression_ne max pe h := + let (tree, h) := norm_expression_ne max pe h in + (PTree.fold (fun pr_op e p_e => (¬ p_e ∨ Pvar e) ∧ pr_op) tree T, h). + +(*Fixpoint encode_expression_ne (max: predicate) (pe: pred_expr_ne) (h: hash_tree) + : (PTree.t pred_op) * hash_tree := + match pe with + | NE.singleton (p, e) => + let (p', h') := hash_value max e h in + (Por (Pnot p) (Pvar p'), h') + | (p, e) ::| pr => + let (p', h') := hash_value max e h in + let (p'', h'') := encode_expression_ne max pr h' in + (Pand (Por (Pnot p) (Pvar p')) p'', h'') + end.*) + +Definition encode_expression (max: predicate) (pe: pred_expr) (h: hash_tree): pred_op * hash_tree := + match pe with + | Psingle e => + let (p, h') := hash_value max e h in (Pvar p, h') + | Plist l => encode_expression_ne max l h + end. + +Fixpoint max_predicate (p: pred_op) : positive := + match p with + | Pvar p => p + | Ptrue => 1 + | Pfalse => 1 + | Pand a b => Pos.max (max_predicate a) (max_predicate b) + | Por a b => Pos.max (max_predicate a) (max_predicate b) + | Pnot a => max_predicate a + end. + +Fixpoint max_pred_expr_ne (pe: pred_expr_ne) : positive := + match pe with + | NE.singleton (p, e) => max_predicate p + | (p, e) ::| pe' => Pos.max (max_predicate p) (max_pred_expr_ne pe') + end. + +Definition max_pred_expr (pe: pred_expr) : positive := + match pe with + | Psingle _ => 1 + | Plist l => max_pred_expr_ne l + end. + +Definition beq_pred_expr (bound: nat) (pe1 pe2: pred_expr) : bool := + match pe1, pe2 with + (*| PEsingleton None e1, PEsingleton None e2 => beq_expression e1 e2 + | PEsingleton (Some p1) e1, PEsingleton (Some p2) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + else false + | PEsingleton (Some p) e1, PEsingleton None e2 + | PEsingleton None e1, PEsingleton (Some p) e2 => + if beq_expression e1 e2 + then match sat_pred_simple bound (Pnot p) with + | Some None => true + | _ => false + end + else false*) + | pe1, pe2 => + let max := Pos.max (max_pred_expr pe1) (max_pred_expr pe2) in + let (p1, h) := encode_expression max pe1 (PTree.empty _) in + let (p2, h') := encode_expression max pe2 h in + match sat_pred_simple bound (Por (Pand p1 (Pnot p2)) (Pand p2 (Pnot p1))) with + | Some None => true + | _ => false + end + end. + +Definition empty : forest := Rtree.empty _. + +Definition check := Rtree.beq (beq_pred_expr 10000). + +Compute (check (empty # (Reg 2) <- + (Plist ((((Pand (Pvar 4) (Pnot (Pvar 4)))), (Ebase (Reg 9))) ::| + (NE.singleton (((Pvar 2)), (Ebase (Reg 3))))))) + (empty # (Reg 2) <- (Plist (NE.singleton (((Por (Pvar 2) (Pand (Pvar 3) (Pnot (Pvar 3))))), + (Ebase (Reg 3))))))). + +Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := + (forall sp op vl m, Op.eval_operation ge sp op vl m = + Op.eval_operation tge sp op vl m) + /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl = + Op.eval_addressing tge sp addr vl). + +Lemma ge_preserved_same: + forall A B ge, @ge_preserved A B A B ge ge. +Proof. unfold ge_preserved; auto. Qed. +#[local] Hint Resolve ge_preserved_same : core. + +Inductive similar {A B} : @ctx A -> @ctx B -> Prop := +| similar_intro : + forall rs ps mem sp ge tge, + ge_preserved ge tge -> + similar (mk_ctx rs ps mem sp ge) (mk_ctx rs ps mem sp tge). + +Lemma unsat_correct1 : + forall a b c, + unsat (Pand a b) -> + sat_predicate a c = true -> + sat_predicate b c = false. +Proof. + unfold unsat in *. intros. + simplify. specialize (H c). + apply andb_false_iff in H. inv H. rewrite H0 in H1. discriminate. + auto. +Qed. + +Lemma unsat_correct2 : + forall a b c, + unsat (Pand a b) -> + sat_predicate b c = true -> + sat_predicate a c = false. +Proof. + unfold unsat in *. intros. + simplify. specialize (H c). + apply andb_false_iff in H. inv H. auto. rewrite H0 in H1. discriminate. +Qed. + +Lemma unsat_not a: unsat (Pand a (Pnot a)). +Proof. unfold unsat; simplify; auto with bool. Qed. + +Lemma unsat_commut a b: unsat (Pand a b) -> unsat (Pand b a). +Proof. unfold unsat; simplify; eauto with bool. Qed. + +Lemma sat_dec a n b: sat_pred n a = Some b -> {sat a} + {unsat a}. +Proof. + unfold sat, unsat. destruct b. + intros. left. destruct s. + exists (Sat.interp_alist x). auto. + intros. tauto. +Qed. + +Lemma sat_equiv : + forall a b, + unsat (Por (Pand a (Pnot b)) (Pand (Pnot a) b)) -> + forall c, sat_predicate a c = sat_predicate b c. +Proof. + unfold unsat. intros. specialize (H c); simplify. + destruct (sat_predicate b c) eqn:X; + destruct (sat_predicate a c) eqn:X2; + crush. +Qed. + +Lemma sat_equiv2 : + forall a b, + unsat (Por (Pand a (Pnot b)) (Pand b (Pnot a))) -> + forall c, sat_predicate a c = sat_predicate b c. +Proof. + unfold unsat. intros. specialize (H c); simplify. + destruct (sat_predicate b c) eqn:X; + destruct (sat_predicate a c) eqn:X2; + crush. +Qed. + +Definition inj_asgn_f a b := if (a =? b)%nat then true else false. + +Lemma inj_asgn_eg : + forall a b, + inj_asgn_f a b = inj_asgn_f a a -> a = b. +Proof. + intros. destruct (Nat.eq_dec a b); subst. + auto. unfold inj_asgn_f in H. apply Nat.eqb_neq in n. + rewrite n in H. rewrite Nat.eqb_refl in H. discriminate. +Qed. + +Lemma inj_asgn : + forall a b, + (forall (f: nat -> bool), f a = f b) -> a = b. +Proof. intros. apply inj_asgn_eg. eauto. Qed. + +Lemma sat_predicate_Pvar_inj : + forall p1 p2, + (forall c, sat_predicate (Pvar p1) c = sat_predicate (Pvar p2) c) -> p1 = p2. +Proof. simplify. apply Pos2Nat.inj. eapply inj_asgn. eauto. Qed. + +Section CORRECT. + + Definition fd := @fundef RTLBlock.bb. + Definition tfd := @fundef RTLPar.bb. + + Context (ictx: @ctx fd) (octx: @ctx tfd) (HSIM: similar ictx octx). + + Lemma sem_value_mem_det: + forall e v v' m m', + (sem_value ictx e v -> sem_value octx e v' -> v = v') + /\ (sem_mem ictx e m -> sem_mem octx e m' -> m = m'). + Proof using HSIM. + induction e using expression_ind2 + with (P0 := fun p => forall v v', + sem_val_list ictx p v -> sem_val_list octx p v' -> v = v'); + inv HSIM; repeat progress simplify; + try solve [match goal with + | H: sem_value _ _ _, H2: sem_value _ _ _ |- _ => inv H; inv H2; auto + | H: sem_mem _ _ _, H2: sem_mem _ _ _ |- _ => inv H; inv H2; auto + | H: sem_val_list _ _ _, H2: sem_val_list _ _ _ |- _ => inv H; inv H2; auto + end]. + - repeat match goal with + | H: sem_value _ _ _ |- _ => inv H + | H: sem_val_list {| ctx_ge := ge; |} ?e ?l1, + H2: sem_val_list {| ctx_ge := tge |} ?e ?l2, + IH: forall _ _, sem_val_list _ _ _ -> sem_val_list _ _ _ -> _ = _ |- _ => + assert (X: l1 = l2) by (apply IH; auto) + | H: ge_preserved _ _ |- _ => inv H + end; crush. + - inv H1. inv H0. simplify. + assert (lv0 = lv). apply IHe; eauto. subst. + inv H. rewrite H1 in H13. + assert (a0 = a1) by crush. subst. + assert (m'1 = m'0). apply IHe0; eauto. subst. + crush. + - inv H0. inv H1. simplify. + assert (lv = lv0). { apply IHe2; eauto. } subst. + assert (a1 = a0). { inv H. rewrite H1 in H12. crush. } subst. + assert (v0 = v1). { apply IHe1; auto. } subst. + assert (m'0 = m'1). { apply IHe3; auto. } subst. + crush. + - inv H0. inv H1. f_equal. apply IHe; auto. + apply IHe0; auto. + Qed. + + Lemma sem_value_det: + forall e v v', + sem_value ictx e v -> sem_value octx e v' -> v = v'. + Proof using HSIM. + intros. eapply sem_value_mem_det; eauto; apply Mem.empty. + Qed. + + Lemma sem_mem_det: + forall e v v', + sem_mem ictx e v -> sem_mem octx e v' -> v = v'. + Proof using HSIM. + intros. eapply sem_value_mem_det; eauto; apply (Vint (Int.repr 0%Z)). + Qed. + + Lemma sem_val_list_det: + forall e l l', + sem_val_list ictx e l -> sem_val_list octx e l' -> l = l'. + Proof using HSIM. + induction e; simplify. + - inv H; inv H0; auto. + - inv H; inv H0. f_equal. eapply sem_value_det; eauto; try apply Mem.empty. + apply IHe; eauto. + Qed. + + Lemma sem_pred_det: + forall e v v', + sem_pred ictx e v -> sem_pred octx e v' -> v = v'. + Proof using HSIM. + try solve [inversion 1]; pose proof sem_value_det; pose proof sem_val_list_det; inv HSIM; simplify. + inv H2; inv H3; auto. assert (lv = lv0) by (eapply H0; eauto). crush. + Qed. + + #[local] Opaque PTree.set. + + Lemma check_correct_sem_value: + forall x x' v v' n, + beq_pred_expr n x x' = true -> + sem_pred_expr sem_value ictx x v -> + sem_pred_expr sem_value octx x' v' -> + v = v'. + Proof. + unfold beq_pred_expr. intros. repeat (destruct_match; try discriminate; []); subst. + unfold sat_pred_simple in *. + repeat destruct_match; try discriminate; []; subst. + assert (X: unsat (Por (Pand p (Pnot p0)) (Pand p0 (Pnot p)))) by eauto. + pose proof (sat_equiv2 _ _ X). + destruct x, x'; simplify. + repeat destruct_match; try discriminate; []. inv Heqp0. inv H0. inv H1. + inv Heqp. + + apply sat_predicate_Pvar_inj in H2; subst. + + assert (e0 = e1) by (eapply hash_present_eq; eauto); subst. + eauto using sem_value_det. + - admit. + - admit. + - admit. + Admitted. + + Lemma check_correct: forall (fa fb : forest) ctx ctx' i, + similar ctx ctx' -> + check fa fb = true -> + @sem fd ctx fa i -> @sem tfd ctx' fb i. + Proof. + intros. + inv H. inv H1. inv H. + (*unfold check, get_forest; intros; + pose proof beq_expression_correct; + match goal with + [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => + apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq + end; + repeat destruct_match; crush. +Qed.*) + Abort. + +End CORRECT. + +Lemma get_empty: + forall r, empty#r = Psingle (Ebase r). +Proof. + intros; unfold get_forest; + destruct_match; auto; [ ]; + match goal with + [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H + end; discriminate. +Qed. + +Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool := + match m1, m2 with + | PTree.Leaf, _ => PTree.bempty m2 + | _, PTree.Leaf => PTree.bempty m1 + | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => + match o1, o2 with + | None, None => true + | Some y1, Some y2 => beqA y1 y2 + | _, _ => false + end + && beq2 beqA l1 l2 && beq2 beqA r1 r2 + end. + +Lemma beq2_correct: + forall A B beqA m1 m2, + @beq2 A B beqA m1 m2 = true <-> + (forall (x: PTree.elt), + match PTree.get x m1, PTree.get x m2 with + | None, None => True + | Some y1, Some y2 => beqA y1 y2 = true + | _, _ => False + end). +Proof. + induction m1; intros. + - simpl. rewrite PTree.bempty_correct. split; intros. + rewrite PTree.gleaf. rewrite H. auto. + generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. + - destruct m2. + + unfold beq2. rewrite PTree.bempty_correct. split; intros. + rewrite H. rewrite PTree.gleaf. auto. + generalize (H x). rewrite PTree.gleaf. + destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. + + simpl. split; intros. + * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). + rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. + destruct x; simpl. apply H1. apply H3. + destruct o; destruct o0; auto || congruence. + * apply andb_true_intro. split. apply andb_true_intro. split. + generalize (H xH); simpl. destruct o; destruct o0; tauto. + apply IHm1_1. intros; apply (H (xO x)). + apply IHm1_2. intros; apply (H (xI x)). +Qed. + +Lemma map1: + forall w dst dst', + dst <> dst' -> + (empty # dst <- w) # dst' = Psingle (Ebase dst'). +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply get_empty. Qed. + +Lemma genmap1: + forall (f : forest) w dst dst', + dst <> dst' -> + (f # dst <- w) # dst' = f # dst'. +Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. + +Lemma map2: + forall (v : pred_expr) x rs, + (rs # x <- v) # x = v. +Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. + +Lemma tri1: + forall x y, + Reg x <> Reg y -> x <> y. +Proof. crush. Qed. diff --git a/src/hls/Array.v b/src/hls/Array.v index dec1335..0f5ae02 100644 --- a/src/hls/Array.v +++ b/src/hls/Array.v @@ -51,7 +51,7 @@ Lemma list_set_spec1 {A : Type} : Proof. induction l; intros; destruct i; crush; firstorder. intuition. Qed. -Hint Resolve list_set_spec1 : array. +#[export] Hint Resolve list_set_spec1 : array. Lemma list_set_spec2 {A : Type} : forall l i (x : A) d, @@ -59,7 +59,7 @@ Lemma list_set_spec2 {A : Type} : Proof. induction l; intros; destruct i; crush; firstorder. intuition. Qed. -Hint Resolve list_set_spec2 : array. +#[export] Hint Resolve list_set_spec2 : array. Lemma list_set_spec3 {A : Type} : forall l i1 i2 (x : A), @@ -68,7 +68,7 @@ Lemma list_set_spec3 {A : Type} : Proof. induction l; intros; destruct i1; destruct i2; crush; firstorder. Qed. -Hint Resolve list_set_spec3 : array. +#[export] Hint Resolve list_set_spec3 : array. Lemma array_set_wf {A : Type} : forall l ln i (x : A), @@ -95,7 +95,7 @@ Proof. unfold array_set. crush. eauto with array. Qed. -Hint Resolve array_set_spec1 : array. +#[export] Hint Resolve array_set_spec1 : array. Lemma array_set_spec2 {A : Type} : forall a i (x : A) d, @@ -107,7 +107,7 @@ Proof. unfold array_set. crush. eauto with array. Qed. -Hint Resolve array_set_spec2 : array. +#[export] Hint Resolve array_set_spec2 : array. Lemma array_set_len {A : Type} : forall a i (x : A), diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 7b9ef9f..784f455 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -30,9 +30,8 @@ Module AssocMap_Properties := Maps.PTree_Properties. Module AssocMapExt. Import AssocMap. - Hint Resolve elements_correct elements_complete - elements_keys_norepet : assocmap. - Hint Resolve gso gss : assocmap. + #[export] Hint Resolve elements_correct elements_complete elements_keys_norepet : assocmap. + #[export] Hint Resolve gso gss : assocmap. Section Operations. @@ -56,7 +55,6 @@ Module AssocMapExt. forall am, merge (empty A) am = am. Proof. auto. Qed. - Hint Resolve merge_base_1 : assocmap. Lemma merge_base_2 : forall am, @@ -66,7 +64,6 @@ Module AssocMapExt. destruct am; trivial. destruct o; trivial. Qed. - Hint Resolve merge_base_2 : assocmap. Lemma merge_add_assoc : forall r am am' v, @@ -75,7 +72,6 @@ Module AssocMapExt. induction r; intros; destruct am; destruct am'; try (destruct o); simpl; try rewrite IHr; try reflexivity. Qed. - Hint Resolve merge_add_assoc : assocmap. Lemma merge_correct_1 : forall am bm k v, @@ -85,7 +81,6 @@ Module AssocMapExt. induction am; intros; destruct k; destruct bm; try (destruct o); simpl; try rewrite gempty in H; try discriminate; try assumption; auto. Qed. - Hint Resolve merge_correct_1 : assocmap. Lemma merge_correct_2 : forall am bm k v, @@ -96,7 +91,6 @@ Module AssocMapExt. induction am; intros; destruct k; destruct bm; try (destruct o); simpl; try rewrite gempty in H; try discriminate; try assumption; auto. Qed. - Hint Resolve merge_correct_2 : assocmap. Lemma merge_correct_3 : forall am bm k, @@ -107,7 +101,6 @@ Module AssocMapExt. induction am; intros; destruct k; destruct bm; try (destruct o); simpl; try rewrite gempty in H; try discriminate; try assumption; auto. Qed. - Hint Resolve merge_correct_3 : assocmap. Definition merge_fold (am bm : t A) : t A := fold_right (fun p a => set (fst p) (snd p) a) bm (elements am). @@ -131,7 +124,6 @@ Module AssocMapExt. apply IHl. contradiction. contradiction. simpl. rewrite gso; try assumption. apply IHl. assumption. inversion H0. subst. assumption. Qed. - Hint Resolve add_assoc : assocmap. Lemma not_in_assoc : forall k v l bm, @@ -146,7 +138,6 @@ Module AssocMapExt. simpl in *; apply Decidable.not_or in H; destruct H. contradiction. rewrite AssocMap.gso; auto. Qed. - Hint Resolve not_in_assoc : assocmap. Lemma elements_iff : forall am k, @@ -159,14 +150,22 @@ Module AssocMapExt. exists (snd x). apply elements_complete. assert (x = (fst x, snd x)) by apply surjective_pairing. rewrite H in H0; assumption. Qed. - Hint Resolve elements_iff : assocmap. + + #[local] Hint Resolve merge_base_1 : core. + #[local] Hint Resolve merge_base_2 : core. + #[local] Hint Resolve merge_add_assoc : core. + #[local] Hint Resolve merge_correct_1 : core. + #[local] Hint Resolve merge_correct_2 : core. + #[local] Hint Resolve merge_correct_3 : core. + #[local] Hint Resolve add_assoc : core. + #[local] Hint Resolve not_in_assoc : core. + #[local] Hint Resolve elements_iff : core. Lemma elements_correct' : forall am k, ~ (exists v, get k am = Some v) <-> ~ List.In k (List.map (@fst _ A) (elements am)). - Proof. auto using not_iff_compat with assocmap. Qed. - Hint Resolve elements_correct' : assocmap. + Proof. auto using not_iff_compat. Qed. Lemma elements_correct_none : forall am k, @@ -176,31 +175,46 @@ Module AssocMapExt. intros. apply elements_correct'. unfold not. intros. destruct H0. rewrite H in H0. discriminate. Qed. - Hint Resolve elements_correct_none : assocmap. Lemma merge_fold_add : forall k v am bm, am ! k = Some v -> (merge_fold am bm) ! k = Some v. Proof. unfold merge_fold; auto with assocmap. Qed. - Hint Resolve merge_fold_add : assocmap. + + #[local] Hint Resolve elements_correct' : core. + #[local] Hint Resolve elements_correct_none : core. + #[local] Hint Resolve merge_fold_add : core. Lemma merge_fold_not_in : forall k v am bm, get k am = None -> get k bm = Some v -> get k (merge_fold am bm) = Some v. - Proof. intros. apply not_in_assoc; auto with assocmap. Qed. - Hint Resolve merge_fold_not_in : assocmap. + Proof. intros. apply not_in_assoc; auto. Qed. Lemma merge_fold_base : forall am, merge_fold (empty A) am = am. Proof. auto. Qed. - Hint Resolve merge_fold_base : assocmap. End Operations. + #[export] Hint Resolve merge_base_1 : assocmap. + #[export] Hint Resolve merge_base_2 : assocmap. + #[export] Hint Resolve merge_add_assoc : assocmap. + #[export] Hint Resolve merge_correct_1 : assocmap. + #[export] Hint Resolve merge_correct_2 : assocmap. + #[export] Hint Resolve merge_correct_3 : assocmap. + #[export] Hint Resolve add_assoc : assocmap. + #[export] Hint Resolve not_in_assoc : assocmap. + #[export] Hint Resolve elements_iff : assocmap. + #[export] Hint Resolve elements_correct' : assocmap. + #[export] Hint Resolve merge_fold_not_in : assocmap. + #[export] Hint Resolve merge_fold_base : assocmap. + #[export] Hint Resolve elements_correct_none : assocmap. + #[export] Hint Resolve merge_fold_add : assocmap. + End AssocMapExt. Import AssocMapExt. diff --git a/src/hls/FunctionalUnits.v b/src/hls/FunctionalUnits.v index e4d51b3..e94b8e8 100644 --- a/src/hls/FunctionalUnits.v +++ b/src/hls/FunctionalUnits.v @@ -21,24 +21,72 @@ Require Import compcert.lib.Maps. Require Import vericert.common.Vericertlib. -Inductive funct_unit: Type := -| SignedDiv (size: positive) (numer denom quot rem: reg): funct_unit -| UnsignedDiv (size: positive) (numer denom quot rem: reg): funct_unit -| Ram (size: positive) (addr d_in d_out wr_en: reg): funct_unit. - -Record funct_units := mk_avail_funct_units { - avail_sdiv: option positive; - avail_udiv: option positive; - avail_ram: option positive; - avail_units: PTree.t funct_unit; +#[local] Open Scope positive. + +Record divider (signed: bool) : Type := + mk_divider { + div_stages: positive; + div_size: positive; + div_numer: reg; + div_denom: reg; + div_quot: reg; + div_rem: reg; + div_ordering: (div_numer < div_denom + /\ div_denom < div_quot + /\ div_quot < div_rem) }. -Definition initial_funct_units := - mk_avail_funct_units None None None (PTree.empty funct_unit). +Arguments div_stages [signed]. +Arguments div_size [signed]. +Arguments div_numer [signed]. +Arguments div_denom [signed]. +Arguments div_quot [signed]. +Arguments div_rem [signed]. + +Record ram := mk_ram { + ram_size: nat; + ram_mem: reg; + ram_en: reg; + ram_u_en: reg; + ram_addr: reg; + ram_wr_en: reg; + ram_d_in: reg; + ram_d_out: reg; + ram_ordering: (ram_addr < ram_en + /\ ram_en < ram_d_in + /\ ram_d_in < ram_d_out + /\ ram_d_out < ram_wr_en + /\ ram_wr_en < ram_u_en) +}. + +Inductive funct_unit: Type := +| SignedDiv: divider true -> funct_unit +| UnsignedDiv: divider false -> funct_unit +| Ram: ram -> funct_unit. + +Definition funct_units := PTree.t funct_unit. + +Record arch := mk_arch { + arch_div: list positive; + arch_sdiv: list positive; + arch_ram: list positive; +}. + +Record resources := mk_resources { + res_funct_units: funct_units; + res_arch: arch; +}. + +Definition initial_funct_units: funct_units := PTree.empty _. + +Definition initial_arch := mk_arch nil nil nil. + +Definition initial_resources := + mk_resources initial_funct_units initial_arch. Definition funct_unit_stages (f: funct_unit) : positive := match f with - | SignedDiv s _ _ _ _ => s - | UnsignedDiv s _ _ _ _ => s + | SignedDiv d => div_stages d + | UnsignedDiv d => div_stages d | _ => 1 end. diff --git a/src/hls/HTL.v b/src/hls/HTL.v index ce7d37e..f16aef5 100644 --- a/src/hls/HTL.v +++ b/src/hls/HTL.v @@ -318,7 +318,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := (State sf mid m st (asr # fin <- (ZToValue 0)) asa). -Hint Constructors step : htl. +#[export] Hint Constructors step : htl. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b m0 m, diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v index d292722..b4291ea 100644 --- a/src/hls/HTLPargen.v +++ b/src/hls/HTLPargen.v @@ -33,11 +33,11 @@ Require Import vericert.hls.RTLPar. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. -Hint Resolve AssocMap.gempty : htlh. -Hint Resolve AssocMap.gso : htlh. -Hint Resolve AssocMap.gss : htlh. -Hint Resolve Ple_refl : htlh. -Hint Resolve Ple_succ : htlh. +#[local] Hint Resolve AssocMap.gempty : htlh. +#[local] Hint Resolve AssocMap.gso : htlh. +#[local] Hint Resolve AssocMap.gss : htlh. +#[local] Hint Resolve Ple_refl : htlh. +#[local] Hint Resolve Ple_succ : htlh. Definition assignment : Type := expr -> expr -> stmnt. @@ -74,10 +74,10 @@ Module HTLState <: State. s1.(st_controllogic)!n = None \/ s2.(st_controllogic)!n = s1.(st_controllogic)!n) -> st_incr s1 s2. - Hint Constructors st_incr : htlh. + #[local] Hint Constructors st_incr : htlh. Definition st_prop := st_incr. - Hint Unfold st_prop : htlh. + #[local] Hint Unfold st_prop : htlh. Lemma st_refl : forall s, st_prop s s. Proof. auto with htlh. Qed. @@ -129,7 +129,7 @@ Lemma declare_reg_state_incr : s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). -Proof. auto with htlh. Qed. +Proof. Admitted. Definition declare_reg (i : option io) (r : reg) (sz : nat) : mon unit := fun s => OK tt (mkstate @@ -641,9 +641,9 @@ Definition add_control_instr_force_state_incr : s.(st_arrdecls) s.(st_datapath) (AssocMap.set n st s.(st_controllogic))). -Abort. +Admitted. -(*Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := +Definition add_control_instr_force (n : node) (st : stmnt) : mon unit := fun s => OK tt (mkstate s.(st_st) @@ -658,7 +658,9 @@ Abort. Fixpoint pred_expr (preg: reg) (p: pred_op) := match p with | Pvar pred => - Vrange preg (Vlit (natToValue pred)) (Vlit (natToValue pred)) + Vrange preg (Vlit (posToValue pred)) (Vlit (posToValue pred)) + | Ptrue => Vlit (ZToValue 1) + | Pfalse => Vlit (ZToValue 0) | Pnot pred => Vunop Vnot (pred_expr preg pred) | Pand p1 p2 => @@ -707,7 +709,7 @@ Lemma create_new_state_state_incr: s.(st_arrdecls) s.(st_datapath) s.(st_controllogic)). -Abort. +Admitted. Definition create_new_state (p: node): mon node := fun s => OK s.(st_freshstate) @@ -875,4 +877,3 @@ Definition transl_program (p : RTLBlockInstr.program) : Errors.res HTL.program : if main_is_internal p then transform_partial_program transl_fundef p else Errors.Error (Errors.msg "Main function is not Internal."). -*) diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index 79fcc53..04595af 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -35,11 +35,11 @@ Require Import vericert.hls.HTL. Require Import vericert.hls.ValueInt. Require Import vericert.hls.Verilog. -Hint Resolve AssocMap.gempty : htlh. -Hint Resolve AssocMap.gso : htlh. -Hint Resolve AssocMap.gss : htlh. -Hint Resolve Ple_refl : htlh. -Hint Resolve Ple_succ : htlh. +#[local] Hint Resolve AssocMap.gempty : htlh. +#[local] Hint Resolve AssocMap.gso : htlh. +#[local] Hint Resolve AssocMap.gss : htlh. +#[local] Hint Resolve Ple_refl : htlh. +#[local] Hint Resolve Ple_succ : htlh. Record state: Type := mkstate { st_st : reg; @@ -86,10 +86,10 @@ Module HTLState <: State. (exists x, (st_externctrl s2) ! n = Some x) -> (n >= st_freshreg s1)%positive) -> st_incr s1 s2. - Hint Constructors st_incr : htlh. + #[export] Hint Constructors st_incr : htlh. Definition st_prop := st_incr. - Hint Unfold st_prop : htlh. + #[export] Hint Unfold st_prop : htlh. Lemma st_refl : forall s, st_prop s s. Proof. split; try solve [ auto with htlh; crush ]. Qed. diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v index 39394b6..77c8c04 100644 --- a/src/hls/HTLgenproof.v +++ b/src/hls/HTLgenproof.v @@ -45,12 +45,12 @@ Set Nested Proofs Allowed. Local Open Scope assocmap. -Hint Resolve Smallstep.forward_simulation_plus : htlproof. -Hint Resolve AssocMap.gss : htlproof. -Hint Resolve AssocMap.gso : htlproof. -Hint Resolve RTL.max_reg_function_def : htlproof. +#[local] Hint Resolve Smallstep.forward_simulation_plus : htlproof. +#[local] Hint Resolve AssocMap.gss : htlproof. +#[local] Hint Resolve AssocMap.gso : htlproof. +#[local] Hint Resolve RTL.max_reg_function_def : htlproof. -Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. +#[local] Hint Unfold find_assocmap AssocMapExt.get_default : htlproof. Hint Constructors val_value_lessdef : htlproof. @@ -59,13 +59,13 @@ Inductive match_assocmaps : RTL.function -> RTL.regset -> assocmap -> Prop := (forall r, Ple r (RTL.max_reg_function f) -> val_value_lessdef (Registers.Regmap.get r rs) am#r) -> match_assocmaps f rs am. -Hint Constructors match_assocmaps : htlproof. +#[local] Hint Constructors match_assocmaps : htlproof. Definition state_st_wf (m : HTL.module) (s : HTL.state) := forall mid st asa asr res, s = HTL.State res mid m st asa asr -> asa!(m.(HTL.mod_st)) = Some (posToValue st). -Hint Unfold state_st_wf : htlproof. +#[local] Hint Unfold state_st_wf : htlproof. Inductive match_arrs (m : HTL.module) (f : RTL.function) (sp : Values.val) (mem : Memory.mem) : Verilog.assocmap_arr -> Prop := @@ -209,7 +209,7 @@ Inductive match_states (ge : RTL.genv) : RTL.state -> HTL.state -> Prop := match_states ge (RTL.Callstate rtl_stk (AST.Internal f) rtl_args mem) (HTL.Callstate htl_stk mid m htl_args). -Hint Constructors match_states : htlproof. +#[local] Hint Constructors match_states : htlproof. Definition match_prog (p: RTL.program) (tp: HTL.program) := Linking.match_program (fun cu f tf => transl_fundef p f = Errors.OK tf) eq p tp /\ @@ -283,7 +283,7 @@ Proof. apply Pos.le_lt_trans with _ _ n in H2. unfold not. intros. subst. eapply Pos.lt_irrefl. eassumption. assumption. Qed. -Hint Resolve regs_lessdef_add_greater : htlproof. +#[local] Hint Resolve regs_lessdef_add_greater : htlproof. Lemma regs_lessdef_add_match : forall f rs am r v v', @@ -302,7 +302,7 @@ Proof. unfold find_assocmap. unfold AssocMapExt.get_default. rewrite AssocMap.gso; eauto. Qed. -Hint Resolve regs_lessdef_add_match : htlproof. +#[local] Hint Resolve regs_lessdef_add_match : htlproof. Lemma list_combine_none : forall n l, @@ -462,7 +462,7 @@ Proof. eexists. unfold Verilog.arr_assocmap_lookup. rewrite H5. reflexivity. Qed. -Hint Resolve arr_lookup_some : htlproof. +#[local] Hint Resolve arr_lookup_some : htlproof. Lemma mem_free_zero_load : forall mem mem' blk chunk sp ptr, Mem.free mem blk 0 0 = Some mem' -> @@ -729,7 +729,7 @@ Section CORRECTNESS. Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof (Genv.senv_transf_partial TRANSL'). - Hint Resolve senv_preserved : htlproof. + #[local] Hint Resolve senv_preserved : htlproof. Lemma ptrofs_inj : forall a b, @@ -1493,7 +1493,7 @@ Section CORRECTNESS. + trans_externctrl. Unshelve. exact tt. Qed. - Hint Resolve transl_inop_correct : htlproof. + #[local] Hint Resolve transl_inop_correct : htlproof. Ltac trans_match_externctrl := unshelve ( @@ -2435,7 +2435,7 @@ Section CORRECTNESS. apply AssocMap.gempty. Unshelve. all: try exact tt; eauto. Qed. - Hint Resolve transl_returnstate_correct : htlproof. + #[local] Hint Resolve transl_returnstate_correct : htlproof. Ltac tac := repeat match goal with @@ -2924,7 +2924,7 @@ Section CORRECTNESS. Unshelve. all: try (exact tt); auto. Admitted. - Hint Resolve transl_iload_correct : htlproof. + #[local] Hint Resolve transl_iload_correct : htlproof. Lemma transl_istore_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -3796,7 +3796,7 @@ Section CORRECTNESS. Unshelve. all: try (exact tt); auto. Qed. - Hint Resolve transl_istore_correct : htlproof. + #[local] Hint Resolve transl_istore_correct : htlproof. Lemma transl_icond_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -3855,7 +3855,7 @@ Section CORRECTNESS. Unshelve. all: exact tt. Qed. - Hint Resolve transl_icond_correct : htlproof. + #[local] Hint Resolve transl_icond_correct : htlproof. (*Lemma transl_ijumptable_correct: forall (s : list RTL.stackframe) (f : RTL.function) (sp : Values.val) (pc : positive) @@ -3871,7 +3871,7 @@ Section CORRECTNESS. Proof. intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE. - Hint Resolve transl_ijumptable_correct : htlproof.*) + #[local] Hint Resolve transl_ijumptable_correct : htlproof.*) Lemma main_tprog_internal : forall b, @@ -3932,7 +3932,7 @@ Section CORRECTNESS. inv Heqm. assumption. Qed. - Hint Resolve transl_initial_states : htlproof. + #[local] Hint Resolve transl_initial_states : htlproof. Lemma transl_final_states : forall (s1 : Smallstep.state (RTL.semantics prog)) @@ -3946,7 +3946,7 @@ Section CORRECTNESS. repeat match goal with [ H : _ |- _ ] => try inv H end. repeat constructor; auto. Qed. - Hint Resolve transl_final_states : htlproof. + #[local] Hint Resolve transl_final_states : htlproof. Theorem transl_step_correct: forall (S1 : RTL.state) t S2, @@ -3957,8 +3957,7 @@ Section CORRECTNESS. Proof. induction 1; eauto with htlproof; try solve [ intros; inv_state ]. Qed. - - Hint Resolve transl_step_correct : htlproof. + #[local] Hint Resolve transl_step_correct : htlproof. Theorem transf_program_correct: Smallstep.forward_simulation (RTL.semantics prog) (HTL.semantics tprog). diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 3c52657..c38b4e6 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -149,16 +149,16 @@ Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop := (clk > rst)%positive -> externctrl_ordering externctrl clk -> tr_module ge f m. -Hint Constructors tr_module : htlspec. +#[local] Hint Constructors tr_module : htlspec. -Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. -Hint Resolve Maps.PTree.elements_correct : htlspec. -Hint Resolve Maps.PTree.gss : htlspec. -Hint Resolve PTree.elements_complete : htlspec. -Hint Resolve -> Z.leb_le : htlspec. +#[local] Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. +#[local] Hint Resolve Maps.PTree.elements_correct : htlspec. +#[local] Hint Resolve Maps.PTree.gss : htlspec. +#[local] Hint Resolve PTree.elements_complete : htlspec. +#[local] Hint Resolve -> Z.leb_le : htlspec. -Hint Unfold block : htlspec. -Hint Unfold nonblock : htlspec. +#[local] Hint Unfold block : htlspec. +#[local] Hint Unfold nonblock : htlspec. Remark bind_inversion: forall (A B: Type) (f: mon A) (g: A -> mon B) @@ -395,7 +395,7 @@ Proof. assert (n < Datatypes.length args)%nat by eauto using nth_error_length. eauto. Qed. -Hint Resolve map_externctrl_params_spec : htlspec. +#[local] Hint Resolve map_externctrl_params_spec : htlspec. Lemma externctrl_params_mapped_trans : forall s s' args params fn, externctrl_params_mapped args params (st_externctrl s) fn -> @@ -493,7 +493,7 @@ Proof. - eapply IHl; eauto. intuition crush. Qed. -Hint Resolve iter_expand_instr_spec : htlspec. +#[local] Hint Resolve iter_expand_instr_spec : htlspec. Lemma map_incr_some : forall {A} map (s s' : st) idx (x : A), (map s) ! idx = Some x -> diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v new file mode 100644 index 0000000..f3c57a8 --- /dev/null +++ b/src/hls/HashTree.v @@ -0,0 +1,438 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 2021 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/>. + *) + +Require Import compcert.lib.Maps. + +Require Import vericert.common.Vericertlib. + +#[local] Open Scope positive. + +#[local] Hint Resolve in_eq : core. +#[local] Hint Resolve in_cons : core. + +Definition max_key {A} (t: PTree.t A) := + fold_right Pos.max 1%positive (map fst (PTree.elements t)). + +Lemma max_key_correct' : + forall l hi, In hi l -> hi <= fold_right Pos.max 1 l. +Proof. + induction l; crush. + inv H. lia. + destruct (Pos.max_dec a (fold_right Pos.max 1 l)); rewrite e. + - apply Pos.max_l_iff in e. + assert (forall a b c, a <= c -> c <= b -> a <= b) by lia. + eapply H; eauto. + - apply IHl; auto. +Qed. + +Lemma max_key_correct : + forall A h_tree hi (c: A), + h_tree ! hi = Some c -> + hi <= max_key h_tree. +Proof. + unfold max_key. intros. apply PTree.elements_correct in H. + apply max_key_correct'. + eapply in_map with (f := fst) in H. auto. +Qed. + +Lemma max_not_present : + forall A k (h: PTree.t A), k > max_key h -> h ! k = None. +Proof. + intros. destruct (h ! k) eqn:?; auto. + apply max_key_correct in Heqo. lia. +Qed. + +Lemma filter_none : + forall A f l (x: A), filter f l = nil -> In x l -> f x = false. +Proof. induction l; crush; inv H0; subst; destruct_match; crush. Qed. + +Lemma filter_set : + forall A l l' f (x: A), + (In x l -> In x l') -> + In x (filter f l) -> + In x (filter f l'). +Proof. + induction l; crush. + destruct_match; crush. inv H0; crush. + apply filter_In. simplify; crush. +Qed. + +Lemma filter_cons_true : + forall A f l (a: A) l', + filter f l = a :: l' -> f a = true. +Proof. + induction l; crush. destruct (f a) eqn:?. + inv H. auto. eapply IHl; eauto. +Qed. + +Lemma PTree_set_elements : + forall A t x x' (c: A), + In x (PTree.elements t) -> + x' <> (fst x) -> + In x (PTree.elements (PTree.set x' c t)). +Proof. + intros. destruct x. + eapply PTree.elements_correct. simplify. + rewrite PTree.gso; auto. apply PTree.elements_complete in H. auto. +Qed. + +Lemma filter_set2 : + forall A x y z (h: PTree.t A), + In z (PTree.elements (PTree.set x y h)) -> + In z (PTree.elements h) \/ fst z = x. +Proof. + intros. destruct z. + destruct (Pos.eq_dec p x); subst. + tauto. + left. apply PTree.elements_correct. apply PTree.elements_complete in H. + rewrite PTree.gso in H; auto. +Qed. + +Lemma in_filter : forall A f l (x: A), In x (filter f l) -> In x l. +Proof. induction l; crush. destruct_match; crush. inv H; crush. Qed. + +Lemma filter_norepet: + forall A f (l: list A), + list_norepet l -> + list_norepet (filter f l). +Proof. + induction l; crush. + inv H. destruct (f a). + constructor. unfold not in *; intros. apply H2. + eapply in_filter; eauto. + apply IHl; auto. + apply IHl; auto. +Qed. + +Lemma filter_norepet2: + forall A B g (l: list (A * B)), + list_norepet (map fst l) -> + list_norepet (map fst (filter g l)). +Proof. + induction l; crush. + inv H. destruct (g a) eqn:?. + simplify. constructor. unfold not in *. intros. + eapply H2. + apply list_in_map_inv in H. simplify; subst. + rewrite H. + apply filter_In in H1. simplify. + apply in_map. eauto. + eapply IHl. eauto. + eapply IHl. eauto. +Qed. + +Module Type Hashable. + + Parameter t: Type. + Parameter eq_dec: forall (t1 t2: t), {t1 = t2} + {t1 <> t2}. + +End Hashable. + +Module HashTree(H: Hashable). + + Import H. + + Definition hash := positive. + Definition hash_tree := PTree.t t. + + Definition find_tree (el: t) (h: hash_tree) : option hash := + match filter (fun x => if eq_dec el (snd x) then true else false) (PTree.elements h) with + | (p, _) :: nil => Some p + | _ => None + end. + + Definition hash_value (max: hash) (e: t) (h: hash_tree): hash * hash_tree := + match find_tree e h with + | Some p => (p, h) + | None => + let nkey := Pos.max max (max_key h) + 1 in + (nkey, PTree.set nkey e h) + end. + + Definition wf_hash_table h_tree := + forall x c, h_tree ! x = Some c -> find_tree c h_tree = Some x. + + Lemma find_tree_correct : + forall c h_tree p, + find_tree c h_tree = Some p -> + h_tree ! p = Some c. + Proof. + intros. + unfold find_tree in H. destruct_match; crush. + destruct_match; simplify. + destruct_match; crush. + assert (In (p, t0) (filter + (fun x : hash * t => + if eq_dec c (snd x) then true else false) (PTree.elements h_tree))). + { setoid_rewrite Heql. constructor; auto. } + apply filter_In in H. simplify. destruct_match; crush. subst. + apply PTree.elements_complete; auto. + Qed. + + Lemma find_tree_unique : + forall c h_tree p p', + find_tree c h_tree = Some p -> + h_tree ! p' = Some c -> + p = p'. + Proof. + intros. + unfold find_tree in H. + repeat (destruct_match; crush; []). + assert (In (p, t0) (filter + (fun x : hash * t => + if eq_dec c (snd x) then true else false) (PTree.elements h_tree))). + { setoid_rewrite Heql. constructor; auto. } + apply filter_In in H. simplify. + destruct (Pos.eq_dec p p'); auto. + exfalso. + destruct_match; subst; crush. + assert (In (p', t0) (PTree.elements h_tree) /\ (fun x : hash * t => + if eq_dec t0 (snd x) then true else false) (p', t0) = true). + { split. apply PTree.elements_correct. auto. setoid_rewrite Heqs. auto. } + apply filter_In in H. setoid_rewrite Heql in H. inv H. simplify. crush. crush. + Qed. + + Lemma hash_no_element' : + forall c h_tree, + find_tree c h_tree = None -> + wf_hash_table h_tree -> + ~ forall x, h_tree ! x = Some c. + Proof. + unfold not, wf_hash_table; intros. + specialize (H1 1). eapply H0 in H1. crush. + Qed. + + Lemma hash_no_element : + forall c h_tree, + find_tree c h_tree = None -> + wf_hash_table h_tree -> + ~ exists x, h_tree ! x = Some c. + Proof. + unfold not, wf_hash_table; intros. + simplify. apply H0 in H2. rewrite H in H2. crush. + Qed. + + Lemma wf_hash_table_set_gso' : + forall h x p0 c', + filter + (fun x : hash * t => + if eq_dec c' (snd x) then true else false) (PTree.elements h) = + (x, p0) :: nil -> + h ! x = Some p0 /\ p0 = c'. + Proof. + intros. + match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + assert (In x (filter f el)) by (rewrite H; crush) + end. + apply filter_In in H0. simplify. destruct_match; subst; crush. + apply PTree.elements_complete; auto. + destruct_match; crush. + Qed. + + Lemma wf_hash_table_set_gso : + forall x x' c' c h, + x <> x' -> + wf_hash_table h -> + find_tree c' h = Some x -> + find_tree c h = None -> + find_tree c' (PTree.set x' c h) = Some x. + Proof. + intros. pose proof H1 as X. unfold find_tree in H1. + destruct_match; crush. + destruct p. destruct l; crush. + apply wf_hash_table_set_gso' in Heql. simplify. + pose proof H2 as Z. apply hash_no_element in H2; auto. + destruct (eq_dec c c'); subst. + { exfalso. eapply H2. econstructor; eauto. } + unfold wf_hash_table in H0. + assert (In (x', c) (PTree.elements (PTree.set x' c h))). + { apply PTree.elements_correct. rewrite PTree.gss; auto. } + assert (In (x, c') (PTree.elements h)). + { apply PTree.elements_correct; auto. } + assert (In (x, c') (PTree.elements (PTree.set x' c h))). + { apply PTree.elements_correct. rewrite PTree.gso; auto. } + pose proof X as Y. + unfold find_tree in X. repeat (destruct_match; crush; []). + match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + assert (In x (filter f el)) by (rewrite H; crush) + end. + apply filter_In in H6. simplify. destruct_match; crush; subst. + unfold find_tree. repeat (destruct_match; crush). + { eapply filter_none in Heql0. + 2: { apply PTree.elements_correct. rewrite PTree.gso; eauto. } + destruct_match; crush. } + + { subst. + repeat match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + learn H; assert (In x (filter f el)) by (rewrite H; crush) + end. + eapply filter_set in H10. rewrite Heql0 in H10. inv H10. simplify. auto. + inv H11. auto. inv H11. intros. eapply PTree_set_elements; auto. } + + { exfalso. subst. + repeat match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + learn H; assert (In x (filter f el)) by (rewrite H; crush) + end. + + pose proof H8 as X2. destruct p1. + pose proof X2 as X4. + apply in_filter in X2. apply PTree.elements_complete in X2. + assert (In (p, t2) (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x' c h)))) by (rewrite H6; eauto). + pose proof H11 as X3. + apply in_filter in H11. apply PTree.elements_complete in H11. + destruct (peq p0 p); subst. + { + assert (list_norepet (map fst (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x' c h))))). + { eapply filter_norepet2. eapply PTree.elements_keys_norepet. } + rewrite Heql0 in H12. simplify. inv H12. eapply H15. apply in_eq. + } + { apply filter_In in X4. simplify. destruct_match; crush; subst. + apply filter_In in X3. simplify. destruct_match; crush; subst. + destruct (peq p x'); subst. + { rewrite PTree.gss in H11; crush. } + { destruct (peq p0 x'); subst. + { rewrite PTree.gss in X2; crush. } + { rewrite PTree.gso in X2 by auto. + rewrite PTree.gso in H11 by auto. + assert (p = p0) by (eapply find_tree_unique; eauto). + crush. } } } } + Qed. + + Lemma wf_hash_table_set : + forall h_tree c v (GT: v > max_key h_tree), + find_tree c h_tree = None -> + wf_hash_table h_tree -> + wf_hash_table (PTree.set v c h_tree). + Proof. + unfold wf_hash_table; simplify. + destruct (peq v x); subst. + pose proof (hash_no_element c h_tree H H0). + rewrite PTree.gss in H1. simplify. + unfold find_tree. + assert (In (x, c0) (PTree.elements (PTree.set x c0 h_tree)) + /\ (fun x : positive * t => if eq_dec c0 (snd x) then true else false) + (x, c0) = true). + { simplify. apply PTree.elements_correct. rewrite PTree.gss. auto. + destruct (eq_dec c0 c0); crush. } + destruct_match. + apply filter_In in H1. rewrite Heql in H1. crush. + apply filter_In in H1. repeat (destruct_match; crush; []). subst. + destruct l. simplify. rewrite Heql in H1. inv H1. inv H3. auto. + crush. + + exfalso. apply H2. destruct p. + pose proof Heql as X. apply filter_cons_true in X. destruct_match; crush; subst. + assert (In (p0, t0) (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x t0 h_tree)))) by (rewrite Heql; eauto). + assert (In (p, t1) (filter + (fun x : positive * t => if eq_dec t0 (snd x) then true else false) + (PTree.elements (PTree.set x t0 h_tree)))) by (rewrite Heql; eauto). + apply filter_In in H4. simplify. destruct_match; crush; subst. + apply in_filter in H3. apply PTree.elements_complete in H5. apply PTree.elements_complete in H3. + assert (list_norepet (map fst (filter + (fun x : positive * t => if eq_dec t1 (snd x) then true else false) + (PTree.elements (PTree.set x t1 h_tree))))). + { eapply filter_norepet2. eapply PTree.elements_keys_norepet. } + rewrite Heql in H4. simplify. + destruct (peq p0 p); subst. + { inv H4. exfalso. eapply H8. eauto. } + destruct (peq x p); subst. + rewrite PTree.gso in H3; auto. econstructor; eauto. + rewrite PTree.gso in H5; auto. econstructor; eauto. + + rewrite PTree.gso in H1; auto. + destruct (eq_dec c c0); subst. + { apply H0 in H1. rewrite H in H1. discriminate. } + apply H0 in H1. + apply wf_hash_table_set_gso; eauto. + Qed. + + Lemma wf_hash_table_distr : + forall m p h_tree h h_tree', + hash_value m p h_tree = (h, h_tree') -> + wf_hash_table h_tree -> + wf_hash_table h_tree'. + Proof. + unfold hash_value; simplify. + destruct_match. + - inv H; auto. + - inv H. apply wf_hash_table_set; try lia; auto. + Qed. + + Lemma wf_hash_table_eq : + forall h_tree a b c, + wf_hash_table h_tree -> + h_tree ! a = Some c -> + h_tree ! b = Some c -> + a = b. + Proof. + unfold wf_hash_table; intros; apply H in H0; eapply find_tree_unique; eauto. + Qed. + + Lemma hash_constant : + forall p h h_tree hi c h_tree' m, + h_tree ! hi = Some c -> + hash_value m p h_tree = (h, h_tree') -> + h_tree' ! hi = Some c. + Proof. + intros. unfold hash_value in H0. destruct_match. + inv H0. eauto. + inv H0. + pose proof H. apply max_key_correct in H0. + rewrite PTree.gso; solve [eauto | lia]. + Qed. + + Lemma find_tree_Some : + forall el h v, + find_tree el h = Some v -> + h ! v = Some el. + Proof. + intros. unfold find_tree in *. + destruct_match; crush. destruct p. + destruct_match; crush. + match goal with + | H: filter ?f ?el = ?x::?xs |- _ => + assert (In x (filter f el)) by (rewrite H; crush) + end. + apply PTree.elements_complete. + apply filter_In in H. inv H. + destruct_match; crush. + Qed. + + Lemma hash_present_eq : + forall m e1 e2 p1 h h', + hash_value m e2 h = (p1, h') -> + h ! p1 = Some e1 -> e1 = e2. + Proof. + intros. unfold hash_value in *. destruct_match. + - inv H. apply find_tree_Some in Heqo. + rewrite Heqo in H0. inv H0. auto. + - inv H. assert (h ! (Pos.max m (max_key h) + 1) = None) + by (apply max_not_present; lia). crush. + Qed. + +End HashTree. diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v index 39d9fd2..f8d404c 100644 --- a/src/hls/IfConversion.v +++ b/src/hls/IfConversion.v @@ -106,7 +106,7 @@ Definition find_blocks_with_cond (c: code) : list (node * bblock) := Definition if_convert_code (p: nat * code) (nb: node * bblock) := let (n, bb) := nb in let (p', c) := p in - let nbb := if_convert_block c p' bb in + let nbb := if_convert_block c (Pos.of_nat p') bb in (S p', PTree.set n nbb c). Definition transf_function (f: function) : function := diff --git a/src/hls/Memorygen.v b/src/hls/Memorygen.v index 864419d..140b5b2 100644 --- a/src/hls/Memorygen.v +++ b/src/hls/Memorygen.v @@ -39,9 +39,9 @@ Require Import vericert.hls.Array. Local Open Scope positive. Local Open Scope assocmap. -Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen. -Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen. -Hint Resolve max_stmnt_lt_module : mgen. +#[local] Hint Resolve max_reg_stmnt_le_stmnt_tree : mgen. +#[local] Hint Resolve max_reg_stmnt_lt_stmnt_tree : mgen. +#[local] Hint Resolve max_stmnt_lt_module : mgen. Lemma int_eq_not_false : forall x, Int.eq x (Int.not x) = false. Proof. @@ -290,7 +290,7 @@ Inductive match_arrs_size : assocmap_arr -> assocmap_arr -> Prop := Definition match_empty_size (m : module) (ar : assocmap_arr) : Prop := match_arrs_size (empty_stack m) ar. -Hint Unfold match_empty_size : mgen. +#[local] Hint Unfold match_empty_size : mgen. Definition disable_ram (ram: option ram) (asr : assocmap_reg) : Prop := match ram with @@ -329,7 +329,7 @@ Inductive match_states : state -> state -> Prop := forall m mid, match_states (Callstate nil mid m nil) (Callstate nil mid (transf_module m) nil). -Hint Constructors match_states : htlproof. +#[local] Hint Constructors match_states : htlproof. Definition empty_stack_ram r := AssocMap.set (ram_mem r) (Array.arr_repeat None (ram_size r)) (AssocMap.empty arr). @@ -339,7 +339,7 @@ Definition empty_stack' len st := Definition match_empty_size' l s (ar : assocmap_arr) : Prop := match_arrs_size (empty_stack' l s) ar. -Hint Unfold match_empty_size : mgen. +#[local] Hint Unfold match_empty_size : mgen. Definition merge_reg_assocs r := Verilog.mkassociations (Verilog.merge_regs (assoc_nonblocking r) (assoc_blocking r)) empty_assocmap. @@ -365,23 +365,23 @@ Ltac mgen_crush := crush; eauto with mgen. Lemma match_assocmaps_equiv : forall p a, match_assocmaps p a a. Proof. constructor; auto. Qed. -Hint Resolve match_assocmaps_equiv : mgen. +#[local] Hint Resolve match_assocmaps_equiv : mgen. Lemma match_arrs_equiv : forall a, match_arrs a a. Proof. econstructor; mgen_crush. Qed. -Hint Resolve match_arrs_equiv : mgen. +#[local] Hint Resolve match_arrs_equiv : mgen. Lemma match_reg_assocs_equiv : forall p a, match_reg_assocs p a a. Proof. destruct a; constructor; mgen_crush. Qed. -Hint Resolve match_reg_assocs_equiv : mgen. +#[local] Hint Resolve match_reg_assocs_equiv : mgen. Lemma match_arr_assocs_equiv : forall a, match_arr_assocs a a. Proof. destruct a; constructor; mgen_crush. Qed. -Hint Resolve match_arr_assocs_equiv : mgen. +#[local] Hint Resolve match_arr_assocs_equiv : mgen. Lemma match_arrs_size_equiv : forall a, match_arrs_size a a. Proof. intros; repeat econstructor; eauto. Qed. -Hint Resolve match_arrs_size_equiv : mgen. +#[local] Hint Resolve match_arrs_size_equiv : mgen. Lemma match_stacks_equiv : forall m s l, @@ -399,7 +399,7 @@ Proof. intros. inv H. constructor. intros. apply H0. lia. Qed. -Hint Resolve match_assocmaps_max1 : mgen. +#[local] Hint Resolve match_assocmaps_max1 : mgen. Lemma match_assocmaps_max2 : forall p p' a b, @@ -409,7 +409,7 @@ Proof. intros. inv H. constructor. intros. apply H0. lia. Qed. -Hint Resolve match_assocmaps_max2 : mgen. +#[local] Hint Resolve match_assocmaps_max2 : mgen. Lemma match_assocmaps_ge : forall p p' a b, @@ -420,21 +420,21 @@ Proof. intros. inv H. constructor. intros. apply H1. lia. Qed. -Hint Resolve match_assocmaps_ge : mgen. +#[local] Hint Resolve match_assocmaps_ge : mgen. Lemma match_reg_assocs_max1 : forall p p' a b, match_reg_assocs (Pos.max p' p) a b -> match_reg_assocs p a b. Proof. intros; inv H; econstructor; mgen_crush. Qed. -Hint Resolve match_reg_assocs_max1 : mgen. +#[local] Hint Resolve match_reg_assocs_max1 : mgen. Lemma match_reg_assocs_max2 : forall p p' a b, match_reg_assocs (Pos.max p p') a b -> match_reg_assocs p a b. Proof. intros; inv H; econstructor; mgen_crush. Qed. -Hint Resolve match_reg_assocs_max2 : mgen. +#[local] Hint Resolve match_reg_assocs_max2 : mgen. Lemma match_reg_assocs_ge : forall p p' a b, @@ -442,7 +442,7 @@ Lemma match_reg_assocs_ge : p <= p' -> match_reg_assocs p a b. Proof. intros; inv H; econstructor; mgen_crush. Qed. -Hint Resolve match_reg_assocs_ge : mgen. +#[local] Hint Resolve match_reg_assocs_ge : mgen. Definition forall_ram (P: reg -> Prop) ram := P (ram_en ram) @@ -461,7 +461,7 @@ Proof. unfold forall_ram; simplify; unfold max_reg_module; repeat apply X; unfold max_reg_ram; rewrite H; try lia. Qed. -Hint Resolve forall_ram_lt : mgen. +#[local] Hint Resolve forall_ram_lt : mgen. Definition exec_all d_s c_s rs1 ar1 rs3 ar3 := exists f rs2 ar2, @@ -553,7 +553,7 @@ Proof. inversion 1; subst; inversion 1; subst; econstructor; intros; apply merge_arr_empty' in H6; auto. Qed. -Hint Resolve merge_arr_empty : mgen. +#[local] Hint Resolve merge_arr_empty : mgen. Lemma merge_arr_empty'': forall m ar s v, @@ -599,7 +599,7 @@ Proof. destruct ar ! s; try discriminate; eauto. apply merge_arr_empty''; auto. apply H2 in H3; auto. Qed. -Hint Resolve merge_arr_empty_match : mgen. +#[local] Hint Resolve merge_arr_empty_match : mgen. Definition ram_present {A: Type} ar r v v' := (assoc_nonblocking ar)!(ram_mem r) = Some v @@ -614,7 +614,7 @@ Lemma find_assoc_get : Proof. intros; unfold find_assocmap, AssocMapExt.get_default; rewrite H; auto. Qed. -Hint Resolve find_assoc_get : mgen. +#[local] Hint Resolve find_assoc_get : mgen. Lemma find_assoc_get2 : forall rs p r v trs, @@ -625,7 +625,7 @@ Lemma find_assoc_get2 : Proof. intros; unfold find_assocmap, AssocMapExt.get_default; rewrite <- H; auto. Qed. -Hint Resolve find_assoc_get2 : mgen. +#[local] Hint Resolve find_assoc_get2 : mgen. Lemma get_assoc_gt : forall A (rs : AssocMap.t A) p r v trs, @@ -634,7 +634,7 @@ Lemma get_assoc_gt : rs ! r = v -> trs ! r = v. Proof. intros. rewrite <- H; auto. Qed. -Hint Resolve get_assoc_gt : mgen. +#[local] Hint Resolve get_assoc_gt : mgen. Lemma expr_runp_matches : forall f rs ar e v, @@ -685,7 +685,7 @@ Proof. assert (forall a b c d, a < b + 1 -> a < Pos.max c (Pos.max d b) + 1) by lia. eapply H5 in H2. apply H4 in H2. auto. auto. Qed. -Hint Resolve expr_runp_matches : mgen. +#[local] Hint Resolve expr_runp_matches : mgen. Lemma expr_runp_matches2 : forall f rs ar e v p, @@ -700,7 +700,7 @@ Proof. assert (max_reg_expr e + 1 <= p) by lia. mgen_crush. Qed. -Hint Resolve expr_runp_matches2 : mgen. +#[local] Hint Resolve expr_runp_matches2 : mgen. Lemma match_assocmaps_gss : forall p rab rab' r rhsval, @@ -714,7 +714,7 @@ Proof. repeat rewrite PTree.gss; auto. repeat rewrite PTree.gso; auto. Qed. -Hint Resolve match_assocmaps_gss : mgen. +#[local] Hint Resolve match_assocmaps_gss : mgen. Lemma match_assocmaps_gt : forall p s ra ra' v, @@ -725,21 +725,21 @@ Proof. intros. inv H0. constructor. intros. rewrite AssocMap.gso; try lia. apply H1; auto. Qed. -Hint Resolve match_assocmaps_gt : mgen. +#[local] Hint Resolve match_assocmaps_gt : mgen. Lemma match_reg_assocs_block : forall p rab rab' r rhsval, match_reg_assocs p rab rab' -> match_reg_assocs p (block_reg r rab rhsval) (block_reg r rab' rhsval). Proof. inversion 1; econstructor; eauto with mgen. Qed. -Hint Resolve match_reg_assocs_block : mgen. +#[local] Hint Resolve match_reg_assocs_block : mgen. Lemma match_reg_assocs_nonblock : forall p rab rab' r rhsval, match_reg_assocs p rab rab' -> match_reg_assocs p (nonblock_reg r rab rhsval) (nonblock_reg r rab' rhsval). Proof. inversion 1; econstructor; eauto with mgen. Qed. -Hint Resolve match_reg_assocs_nonblock : mgen. +#[local] Hint Resolve match_reg_assocs_nonblock : mgen. Lemma some_inj : forall A (x: A) y, @@ -772,7 +772,7 @@ Proof. apply nth_error_None. destruct a. simplify. lia. Qed. -Hint Resolve array_get_error_bound_gt : mgen. +#[local] Hint Resolve array_get_error_bound_gt : mgen. Lemma array_get_error_each : forall A addr i (v : A) a x, @@ -790,7 +790,7 @@ Proof. rewrite <- array_set_len. rewrite <- H. lia. repeat rewrite array_gso; auto. Qed. -Hint Resolve array_get_error_each : mgen. +#[local] Hint Resolve array_get_error_each : mgen. Lemma match_arrs_gss : forall ar ar' r v i, @@ -839,21 +839,21 @@ Proof. destruct ar!r eqn:?; repeat mag_tac; crush. apply H1 in Heqo. repeat mag_tac; auto. Qed. -Hint Resolve match_arrs_gss : mgen. +#[local] Hint Resolve match_arrs_gss : mgen. Lemma match_arr_assocs_block : forall rab rab' r i rhsval, match_arr_assocs rab rab' -> match_arr_assocs (block_arr r i rab rhsval) (block_arr r i rab' rhsval). Proof. inversion 1; econstructor; eauto with mgen. Qed. -Hint Resolve match_arr_assocs_block : mgen. +#[local] Hint Resolve match_arr_assocs_block : mgen. Lemma match_arr_assocs_nonblock : forall rab rab' r i rhsval, match_arr_assocs rab rab' -> match_arr_assocs (nonblock_arr r i rab rhsval) (nonblock_arr r i rab' rhsval). Proof. inversion 1; econstructor; eauto with mgen. Qed. -Hint Resolve match_arr_assocs_nonblock : mgen. +#[local] Hint Resolve match_arr_assocs_nonblock : mgen. Lemma match_states_same : forall f rs1 ar1 c rs2 ar2 p, @@ -933,7 +933,7 @@ Proof. rewrite <- H2; eauto. rewrite <- H; eauto. Qed. -Hint Resolve match_reg_assocs_merge : mgen. +#[local] Hint Resolve match_reg_assocs_merge : mgen. Lemma transf_not_changed : forall state ram n d c i d_s c_s, @@ -1013,7 +1013,7 @@ Proof. intros. apply AssocMapExt.elements_correct' in H. unfold not in *. destruct am ! k eqn:?; auto. exfalso. apply H. eexists. auto. Qed. -Hint Resolve elements_correct_none : assocmap. +#[local] Hint Resolve elements_correct_none : assocmap. Lemma max_index_2 : forall A (d: AssocMap.t A) i, i > max_pc d -> d ! i = None. @@ -1068,14 +1068,14 @@ Proof. intros; unfold empty_stack, transf_module; repeat destruct_match; mgen_crush. Qed. -Hint Resolve empty_arrs_match : mgen. +#[local] Hint Resolve empty_arrs_match : mgen. Lemma max_module_stmnts : forall m, Pos.max (max_stmnt_tree (mod_controllogic m)) (max_stmnt_tree (mod_datapath m)) < max_reg_module m + 1. Proof. intros. unfold max_reg_module. lia. Qed. -Hint Resolve max_module_stmnts : mgen. +#[local] Hint Resolve max_module_stmnts : mgen. Lemma transf_module_code : forall m, @@ -1094,36 +1094,36 @@ Lemma transf_module_code : = ((mod_datapath (transf_module m)), mod_controllogic (transf_module m)). Proof. unfold transf_module; intros; repeat destruct_match; crush. apply surjective_pairing. Qed. -Hint Resolve transf_module_code : mgen. +#[local] Hint Resolve transf_module_code : mgen. Lemma transf_module_code_ram : forall m r, mod_ram m = Some r -> transf_module m = m. Proof. unfold transf_module; intros; repeat destruct_match; crush. Qed. -Hint Resolve transf_module_code_ram : mgen. +#[local] Hint Resolve transf_module_code_ram : mgen. Lemma mod_reset_lt : forall m, mod_reset m < max_reg_module m + 1. Proof. intros; unfold max_reg_module; lia. Qed. -Hint Resolve mod_reset_lt : mgen. +#[local] Hint Resolve mod_reset_lt : mgen. Lemma mod_finish_lt : forall m, mod_finish m < max_reg_module m + 1. Proof. intros; unfold max_reg_module; lia. Qed. -Hint Resolve mod_finish_lt : mgen. +#[local] Hint Resolve mod_finish_lt : mgen. Lemma mod_return_lt : forall m, mod_return m < max_reg_module m + 1. Proof. intros; unfold max_reg_module; lia. Qed. -Hint Resolve mod_return_lt : mgen. +#[local] Hint Resolve mod_return_lt : mgen. Lemma mod_start_lt : forall m, mod_start m < max_reg_module m + 1. Proof. intros; unfold max_reg_module; lia. Qed. -Hint Resolve mod_start_lt : mgen. +#[local] Hint Resolve mod_start_lt : mgen. Lemma mod_stk_lt : forall m, mod_stk m < max_reg_module m + 1. Proof. intros; unfold max_reg_module; lia. Qed. -Hint Resolve mod_stk_lt : mgen. +#[local] Hint Resolve mod_stk_lt : mgen. Lemma mod_st_lt : forall m, mod_st m < max_reg_module m + 1. Proof. intros; unfold max_reg_module; lia. Qed. -Hint Resolve mod_st_lt : mgen. +#[local] Hint Resolve mod_st_lt : mgen. Lemma mod_reset_modify : forall m ar ar' v, @@ -1135,7 +1135,7 @@ Proof. unfold transf_module; repeat destruct_match; simplify; rewrite <- H0; eauto with mgen. Qed. -Hint Resolve mod_reset_modify : mgen. +#[local] Hint Resolve mod_reset_modify : mgen. Lemma mod_finish_modify : forall m ar ar' v, @@ -1147,7 +1147,7 @@ Proof. unfold transf_module; repeat destruct_match; simplify; rewrite <- H0; eauto with mgen. Qed. -Hint Resolve mod_finish_modify : mgen. +#[local] Hint Resolve mod_finish_modify : mgen. Lemma mod_return_modify : forall m ar ar' v, @@ -1159,7 +1159,7 @@ Proof. unfold transf_module; repeat destruct_match; simplify; rewrite <- H0; eauto with mgen. Qed. -Hint Resolve mod_return_modify : mgen. +#[local] Hint Resolve mod_return_modify : mgen. Lemma mod_start_modify : forall m ar ar' v, @@ -1171,7 +1171,7 @@ Proof. unfold transf_module; repeat destruct_match; simplify; rewrite <- H0; eauto with mgen. Qed. -Hint Resolve mod_start_modify : mgen. +#[local] Hint Resolve mod_start_modify : mgen. Lemma mod_st_modify : forall m ar ar' v, @@ -1183,7 +1183,7 @@ Proof. unfold transf_module; repeat destruct_match; simplify; rewrite <- H0; eauto with mgen. Qed. -Hint Resolve mod_st_modify : mgen. +#[local] Hint Resolve mod_st_modify : mgen. Lemma match_arrs_read : forall ra ra' addr v mem, @@ -1198,7 +1198,7 @@ Proof. inv H0. eapply H1 in Heqo0. inv Heqo0. inv H0. unfold arr in *. rewrite H3 in Heqo. discriminate. Qed. -Hint Resolve match_arrs_read : mgen. +#[local] Hint Resolve match_arrs_read : mgen. Lemma match_reg_implies_equal : forall ra ra' p a b c, @@ -1211,7 +1211,7 @@ Proof. inv H2. destruct (ra ! a) eqn:?; destruct (ra ! b) eqn:?; repeat rewrite <- H3 by lia; rewrite Heqo; rewrite Heqo0; auto. Qed. -Hint Resolve match_reg_implies_equal : mgen. +#[local] Hint Resolve match_reg_implies_equal : mgen. Lemma exec_ram_same : forall rs1 ar1 ram rs2 ar2 p, @@ -1260,7 +1260,7 @@ Proof. erewrite AssocMapExt.merge_correct_3; mgen_crush. erewrite AssocMapExt.merge_correct_3; mgen_crush. Qed. -Hint Resolve match_assocmaps_merge : mgen. +#[local] Hint Resolve match_assocmaps_merge : mgen. Lemma list_combine_nth_error1 : forall l l' addr v, @@ -1418,7 +1418,7 @@ Proof. unfold Verilog.arr in *. rewrite Heqo. rewrite Heqo0. auto. Qed. -Hint Resolve match_arrs_merge : mgen. +#[local] Hint Resolve match_arrs_merge : mgen. Lemma match_empty_size_merge : forall nasa2 basa2 m, @@ -1457,7 +1457,7 @@ Proof. apply H3 in H6. unfold merge_arrs. rewrite AssocMap.gcombine by auto. setoid_rewrite H0. setoid_rewrite H6. auto. Qed. -Hint Resolve match_empty_size_merge : mgen. +#[local] Hint Resolve match_empty_size_merge : mgen. Lemma match_empty_size_match : forall m nasa2 basa2, @@ -1483,7 +1483,7 @@ Proof. end; simplify. inversion 1; inversion 1; constructor; simplify; repeat match_empty_size_match_solve. Qed. -Hint Resolve match_empty_size_match : mgen. +#[local] Hint Resolve match_empty_size_match : mgen. Lemma match_get_merge : forall p ran ran' rab rab' s v, @@ -1497,7 +1497,7 @@ Proof. assert (X: match_assocmaps p (merge_regs ran rab) (merge_regs ran' rab')) by auto with mgen. inv X. rewrite <- H3; auto. Qed. -Hint Resolve match_get_merge : mgen. +#[local] Hint Resolve match_get_merge : mgen. Ltac masrp_tac := match goal with @@ -1556,7 +1556,7 @@ Proof. apply H2 in H5. auto. apply H2 in H5. auto. Unshelve. auto. Qed. -Hint Resolve match_empty_assocmap_set : mgen. +#[local] Hint Resolve match_empty_assocmap_set : mgen. Lemma match_arrs_size_stmnt_preserved : forall m f rs1 ar1 ar2 c rs2, @@ -1589,7 +1589,7 @@ Proof. assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *. eapply match_arrs_size_stmnt_preserved; mgen_crush. Qed. -Hint Resolve match_arrs_size_stmnt_preserved2 : mgen. +#[local] Hint Resolve match_arrs_size_stmnt_preserved2 : mgen. Lemma match_arrs_size_ram_preserved : forall m rs1 ar1 ar2 ram rs2, @@ -1612,7 +1612,7 @@ Proof. apply H9 in H17; auto. apply H9 in H17; auto. Unshelve. eauto. Qed. -Hint Resolve match_arrs_size_ram_preserved : mgen. +#[local] Hint Resolve match_arrs_size_ram_preserved : mgen. Lemma match_arrs_size_ram_preserved2 : forall m rs1 na na' ba ba' ram rs2, @@ -1630,7 +1630,7 @@ Proof. assert (X4: ba = (assoc_blocking ar1)) by (rewrite Heqar1; auto). rewrite X4 in *. eapply match_arrs_size_ram_preserved; mgen_crush. Qed. -Hint Resolve match_arrs_size_ram_preserved2 : mgen. +#[local] Hint Resolve match_arrs_size_ram_preserved2 : mgen. Lemma empty_stack_m : forall m, empty_stack m = empty_stack' (mod_stk_len m) (mod_stk m). @@ -1926,7 +1926,7 @@ Lemma match_arrs_size_assoc : match_arrs_size a b -> match_arrs_size b a. Proof. inversion 1; constructor; crush; split; apply H2. Qed. -Hint Resolve match_arrs_size_assoc : mgen. +#[local] Hint Resolve match_arrs_size_assoc : mgen. Lemma match_arrs_merge_set2 : forall rab rab' ran ran' s m i v, @@ -2015,11 +2015,11 @@ Qed. Definition all_match_empty_size m ar := match_empty_size m (assoc_nonblocking ar) /\ match_empty_size m (assoc_blocking ar). -Hint Unfold all_match_empty_size : mgen. +#[local] Hint Unfold all_match_empty_size : mgen. Definition match_module_to_ram m ram := ram_size ram = mod_stk_len m /\ ram_mem ram = mod_stk m. -Hint Unfold match_module_to_ram : mgen. +#[local] Hint Unfold match_module_to_ram : mgen. Lemma zip_range_forall_le : forall A (l: list A) n, Forall (Pos.le n) (map snd (zip_range n l)). @@ -2409,7 +2409,7 @@ Proof. unfold merge_arrs. rewrite AssocMap.gcombine; auto. setoid_rewrite H6. setoid_rewrite H7. auto. Qed. -Hint Resolve merge_arr_empty2 : mgen. +#[local] Hint Resolve merge_arr_empty2 : mgen. Lemma find_assocmap_gso : forall ar x y v, x <> y -> (ar # y <- v) # x = ar # x. @@ -2945,11 +2945,11 @@ Proof. unfold disable_ram, find_assocmap, AssocMapExt.get_default; intros; repeat rewrite AssocMap.gso by lia; auto. Qed. -Hint Resolve disable_ram_set_gso : mgen. +#[local] Hint Resolve disable_ram_set_gso : mgen. Lemma disable_ram_None rs : disable_ram None rs. Proof. unfold disable_ram; auto. Qed. -Hint Resolve disable_ram_None : mgen. +#[local] Hint Resolve disable_ram_None : mgen. Lemma init_regs_equal_empty l st : Forall (Pos.gt st) l -> (init_regs nil l) ! st = None. @@ -2970,7 +2970,7 @@ Section CORRECTNESS. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof using TRANSL. intros. eapply (Genv.find_symbol_match TRANSL). Qed. - Hint Resolve symbols_preserved : mgen. + #[local] Hint Resolve symbols_preserved : mgen. Lemma function_ptr_translated: forall (b: Values.block) (f: fundef), @@ -2981,7 +2981,7 @@ Section CORRECTNESS. intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Hint Resolve function_ptr_translated : mgen. + #[local] Hint Resolve function_ptr_translated : mgen. Lemma functions_translated: forall (v: Values.val) (f: fundef), @@ -2992,12 +2992,12 @@ Section CORRECTNESS. intros. exploit (Genv.find_funct_match TRANSL); eauto. intros (cu & tf & P & Q & R); exists tf; auto. Qed. - Hint Resolve functions_translated : mgen. + #[local] Hint Resolve functions_translated : mgen. Lemma senv_preserved: Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge). Proof (Genv.senv_transf TRANSL). - Hint Resolve senv_preserved : mgen. + #[local] Hint Resolve senv_preserved : mgen. Theorem transf_step_correct: forall (S1 : state) t S2, @@ -3165,7 +3165,7 @@ Section CORRECTNESS. (* simplify. unfold max_reg_module. lia. *) (* simplify. unfold max_reg_module. lia. *) Admitted. - Hint Resolve transf_step_correct : mgen. + #[local] Hint Resolve transf_step_correct : mgen. Lemma transf_initial_states : forall s1 : state, @@ -3186,7 +3186,7 @@ Section CORRECTNESS. - replace (prog_main prog) with (prog_main tprog) by (eapply Linking.match_program_main; eauto). econstructor. Qed. - Hint Resolve transf_initial_states : mgen. + #[local] Hint Resolve transf_initial_states : mgen. Lemma transf_final_states : forall (s1 : state) @@ -3198,7 +3198,7 @@ Section CORRECTNESS. Proof using TRANSL. intros. inv H0. inv H. inv STACKS. unfold valueToInt. constructor. auto. Qed. - Hint Resolve transf_final_states : mgen. + #[local] Hint Resolve transf_final_states : mgen. Theorem transf_program_correct: Smallstep.forward_simulation (semantics prog) (semantics tprog). diff --git a/src/hls/Partition.ml b/src/hls/Partition.ml new file mode 100644 index 0000000..19c6048 --- /dev/null +++ b/src/hls/Partition.ml @@ -0,0 +1,124 @@ + (* + * Vericert: Verified high-level synthesis. + * Copyright (C) 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/>. + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlockInstr +open RTLBlock + +(* Assuming that the nodes of the CFG [code] are numbered in reverse postorder (cf. pass + [Renumber]), an edge from [n] to [s] is a normal edge if [s < n] and a back-edge otherwise. *) +let find_edge i n = + let succ = RTL.successors_instr i in + let filt = List.filter (fun s -> P.lt n s || P.lt s (P.pred n)) succ in + ((match filt with [] -> [] | _ -> [n]), filt) + +let find_edges c = + PTree.fold (fun l n i -> + let f = find_edge i n in + (List.append (fst f) (fst l), List.append (snd f) (snd l))) c ([], []) + +let prepend_instr i = function + | {bb_body = bb; bb_exit = e} -> {bb_body = (i :: bb); bb_exit = e} + +let translate_inst = function + | RTL.Inop _ -> Some RBnop + | RTL.Iop (op, ls, dst, _) -> Some (RBop (None, op, ls, dst)) + | RTL.Iload (m, addr, ls, dst, _) -> Some (RBload (None, m, addr, ls, dst)) + | RTL.Istore (m, addr, ls, src, _) -> Some (RBstore (None, m, addr, ls, src)) + | _ -> None + +let translate_cfi = function + | RTL.Icall (s, r, ls, dst, n) -> Some (RBcall (s, r, ls, dst, n)) + | RTL.Itailcall (s, r, ls) -> Some (RBtailcall (s, r, ls)) + | RTL.Ibuiltin (e, ls, r, n) -> Some (RBbuiltin (e, ls, r, n)) + | RTL.Icond (c, ls, dst1, dst2) -> Some (RBcond (c, ls, dst1, dst2)) + | RTL.Ijumptable (r, ls) -> Some (RBjumptable (r, ls)) + | RTL.Ireturn r -> Some (RBreturn r) + | _ -> None + +let rec next_bblock_from_RTL is_start e (c : RTL.code) s i = + let succ = List.map (fun i -> (i, PTree.get i c)) (RTL.successors_instr i) in + let trans_inst = (translate_inst i, translate_cfi i) in + match trans_inst, succ with + | (None, Some i'), _ -> + if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = RBgoto s } + else + Errors.OK { bb_body = []; bb_exit = i' } + | (Some i', None), (s', Some i_n)::[] -> + if List.exists (fun x -> x = s) (fst e) then + Errors.OK { bb_body = [i']; bb_exit = RBgoto s' } + else if List.exists (fun x -> x = s) (snd e) && not is_start then + Errors.OK { bb_body = []; bb_exit = RBgoto s } + else begin + match next_bblock_from_RTL false e c s' i_n with + | Errors.OK bb -> + Errors.OK (prepend_instr i' bb) + | Errors.Error msg -> Errors.Error msg + end + | _, _ -> + Errors.Error (Errors.msg (coqstring_of_camlstring "next_bblock_from_RTL went wrong.")) + +let rec traverseacc f l c = + match l with + | [] -> Errors.OK c + | x::xs -> + match f x c with + | Errors.Error msg -> Errors.Error msg + | Errors.OK x' -> + match traverseacc f xs x' with + | Errors.Error msg -> Errors.Error msg + | Errors.OK xs' -> Errors.OK xs' + +let rec translate_all edge c s res = + let c_bb, translated = res in + if List.exists (fun x -> P.eq x s) translated then Errors.OK (c_bb, translated) else + (match PTree.get s c with + | None -> Errors.Error (Errors.msg (coqstring_of_camlstring "Could not translate all.")) + | Some i -> + match next_bblock_from_RTL true edge c s i with + | Errors.Error msg -> Errors.Error msg + | Errors.OK {bb_body = bb; bb_exit = e} -> + let succ = List.filter (fun x -> P.lt x s) (successors_instr e) in + (match traverseacc (translate_all edge c) succ (c_bb, s :: translated) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c', t') -> + Errors.OK (PTree.set s {bb_body = bb; bb_exit = e} c', t'))) + +(* Partition a function and transform it into RTLBlock. *) +let function_from_RTL f = + let e = find_edges f.RTL.fn_code in + match translate_all e f.RTL.fn_code f.RTL.fn_entrypoint (PTree.empty, []) with + | Errors.Error msg -> Errors.Error msg + | Errors.OK (c, _) -> + Errors.OK { fn_sig = f.RTL.fn_sig; + fn_stacksize = f.RTL.fn_stacksize; + fn_params = f.RTL.fn_params; + fn_entrypoint = f.RTL.fn_entrypoint; + fn_code = c + } + +let partition = function_from_RTL diff --git a/src/hls/PrintExpression.ml b/src/hls/PrintExpression.ml new file mode 100644 index 0000000..df5dc37 --- /dev/null +++ b/src/hls/PrintExpression.ml @@ -0,0 +1,40 @@ +(*open Printf +open Camlcoq +open Datatypes +open Maps +open PrintAST +open RTLPargen + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let pred pp r = + fprintf pp "p%d" (P.to_int r) + +let print_resource pp = function + | Reg r -> reg pp r + | Pred r -> pred pp r + | Mem -> fprintf pp "M" + +let rec to_expr_list = function + | Enil -> [] + | Econs (e, elist) -> e :: to_expr_list elist + +let rec print_expression pp = function + | Ebase r -> print_resource pp r + | Eop (op, elist, e) -> + PrintOp.print_operation print_expression pp (op, to_expr_list elist); + Printf.printf "; "; + print_expression pp e + | Eload (chunk, addr, elist, e) -> + fprintf pp "%s[%a]; " (name_of_chunk chunk) (PrintOp.print_addressing print_expression) (addr, to_expr_list elist); + print_expression pp e + | Estore (e, chunk, addr, elist, e') -> + fprintf pp "%s[%a] = %a; " (name_of_chunk chunk) + (PrintOp.print_addressing print_expression) (addr, to_expr_list elist) + print_expression e; + print_expression pp e + | Esetpred (cond, elist, e) -> + fprintf pp "%a; " (PrintOp.print_condition print_expression) (cond, to_expr_list elist); + print_expression pp e +*) diff --git a/src/hls/PrintHTL.ml b/src/hls/PrintHTL.ml index 3bce337..79221cf 100644 --- a/src/hls/PrintHTL.ml +++ b/src/hls/PrintHTL.ml @@ -140,6 +140,6 @@ let print_if passno prog = match !destination with | None -> () | Some f -> - let oc = open_out (f ^ "." ^ Z.to_string passno) in - print_program oc prog; - close_out oc + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc diff --git a/src/hls/PrintRTLBlock.ml b/src/hls/PrintRTLBlock.ml new file mode 100644 index 0000000..8fef401 --- /dev/null +++ b/src/hls/PrintRTLBlock.ml @@ -0,0 +1,72 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open RTLBlock +open PrintAST +open PrintRTLBlockInstr + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (print_bblock_body pp) i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if passno prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc diff --git a/src/hls/PrintRTLBlockInstr.ml b/src/hls/PrintRTLBlockInstr.ml new file mode 100644 index 0000000..979ca38 --- /dev/null +++ b/src/hls/PrintRTLBlockInstr.ml @@ -0,0 +1,87 @@ +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open PrintAST + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let pred pp r = + fprintf pp "p%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let rec print_pred_op pp = function + | Pvar p -> pred pp p + | Pnot p -> fprintf pp "(~ %a)" print_pred_op p + | Pand (p1, p2) -> fprintf pp "(%a & %a)" print_pred_op p1 print_pred_op p2 + | Por (p1, p2) -> fprintf pp "(%a | %a)" print_pred_op p1 print_pred_op p2 + +let print_pred_option pp = function + | Some x -> fprintf pp "(%a)" print_pred_op x + | None -> () + +let print_bblock_body pp i = + fprintf pp "\t\t"; + match i with + | RBnop -> fprintf pp "nop\n" + | RBop(p, op, ls, dst) -> + fprintf pp "%a %a = %a\n" + print_pred_option p reg dst (PrintOp.print_operation reg) (op, ls) + | RBload(p, chunk, addr, args, dst) -> + fprintf pp "%a %a = %s[%a]\n" + print_pred_option p reg dst (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + | RBstore(p, chunk, addr, args, src) -> + fprintf pp "%a %s[%a] = %a\n" + print_pred_option p + (name_of_chunk chunk) + (PrintOp.print_addressing reg) (addr, args) + reg src + | RBsetpred (c, args, p) -> + fprintf pp "%a = %a\n" + pred p + (PrintOp.print_condition reg) (c, args) + +let rec print_bblock_exit pp i = + fprintf pp "\t\t"; + match i with + | RBcall(_, fn, args, res, _) -> + fprintf pp "%a = %a(%a)\n" + reg res ros fn regs args; + | RBtailcall(_, fn, args) -> + fprintf pp "tailcall %a(%a)\n" + ros fn regs args + | RBbuiltin(ef, args, res, _) -> + fprintf pp "%a = %s(%a)\n" + (print_builtin_res reg) res + (name_of_external ef) + (print_builtin_args reg) args + | RBcond(cond, args, s1, s2) -> + fprintf pp "if (%a) goto %d else goto %d\n" + (PrintOp.print_condition reg) (cond, args) + (P.to_int s1) (P.to_int s2) + | RBjumptable(arg, tbl) -> + let tbl = Array.of_list tbl in + fprintf pp "jumptable (%a)\n" reg arg; + for i = 0 to Array.length tbl - 1 do + fprintf pp "\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done + | RBreturn None -> + fprintf pp "return\n" + | RBreturn (Some arg) -> + fprintf pp "return %a\n" reg arg + | RBgoto n -> + fprintf pp "goto %d\n" (P.to_int n) + | RBpred_cf (p, c1, c2) -> + fprintf pp "if %a then (%a) else (%a)\n" print_pred_op p print_bblock_exit c1 print_bblock_exit c2 diff --git a/src/hls/PrintRTLPar.ml b/src/hls/PrintRTLPar.ml new file mode 100644 index 0000000..ab93fa5 --- /dev/null +++ b/src/hls/PrintRTLPar.ml @@ -0,0 +1,74 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Pretty-printers for RTL code *) + +open Printf +open Camlcoq +open Datatypes +open Maps +open AST +open RTLBlockInstr +open RTLPar +open PrintAST +open PrintRTLBlockInstr + +(* Printing of RTL code *) + +let reg pp r = + fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [r] -> reg pp r + | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_bblock pp (pc, i) = + fprintf pp "%5d:{\n" pc; + List.iter (fun x -> fprintf pp "{\n"; + List.iter (fun x -> fprintf pp "( "; List.iter (print_bblock_body pp) x; fprintf pp " )") x; + fprintf pp "}\n") i.bb_body; + print_bblock_exit pp i.bb_exit; + fprintf pp "\t}\n\n" + +let print_function pp id f = + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; + let instrs = + List.sort + (fun (pc1, _) (pc2, _) -> compare pc2 pc1) + (List.rev_map + (fun (pc, i) -> (P.to_int pc, i)) + (PTree.elements f.fn_code)) in + List.iter (print_bblock pp) instrs; + fprintf pp "}\n\n" + +let print_globdef pp (id, gd) = + match gd with + | Gfun(Internal f) -> print_function pp id f + | _ -> () + +let print_program pp (prog: program) = + List.iter (print_globdef pp) prog.prog_defs + +let destination : string option ref = ref None + +let print_if passno prog = + match !destination with + | None -> () + | Some f -> + let oc = open_out (f ^ "." ^ Z.to_string passno) in + print_program oc prog; + close_out oc diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v index 6a3487a..bf5c37a 100644 --- a/src/hls/RTLBlock.v +++ b/src/hls/RTLBlock.v @@ -58,11 +58,11 @@ Section RELSEM. Inductive step: state -> trace -> state -> Prop := | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb, + forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_list sp (InstrState rs m) bb.(bb_body) (InstrState rs' m') -> - step_cf_instr ge (State s f sp pc rs' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs m) t s' + step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> + step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> + step (State s f sp pc rs pr m) t s' | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -72,6 +72,7 @@ Section RELSEM. (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) + (PMap.init false) m') | exec_function_external: forall s ef args res t m m', @@ -79,9 +80,9 @@ Section RELSEM. step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: - forall res f sp pc rs s vres m, - step (Returnstate (Stackframe res f sp pc rs :: s) vres m) - E0 (State s f sp pc (rs#res <- vres) m). + forall res f sp pc rs s vres m pr, + step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) pr m). End RELSEM. diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v index 3fab464..56048d4 100644 --- a/src/hls/RTLBlockInstr.v +++ b/src/hls/RTLBlockInstr.v @@ -34,17 +34,29 @@ Require Import vericert.hls.Sat. Local Open Scope rtl. Definition node := positive. -Definition predicate := nat. +Definition predicate := positive. Inductive pred_op : Type := | Pvar: predicate -> pred_op +| Ptrue: pred_op +| Pfalse: pred_op | Pnot: pred_op -> pred_op | Pand: pred_op -> pred_op -> pred_op | Por: pred_op -> pred_op -> pred_op. +Declare Scope pred_op. + +Notation "A ∧ B" := (Pand A B) (at level 20) : pred_op. +Notation "A ∨ B" := (Por A B) (at level 25) : pred_op. +Notation "⟂" := (Pfalse) : pred_op. +Notation "'T'" := (Ptrue) : pred_op. +Notation "¬ A" := (Pnot A) (at level 15) : pred_op. + Fixpoint sat_predicate (p: pred_op) (a: asgn) : bool := match p with - | Pvar p' => a p' + | Pvar p' => a (Pos.to_nat p') + | Ptrue => true + | Pfalse => false | Pnot p' => negb (sat_predicate p' a) | Pand p1 p2 => sat_predicate p1 a && sat_predicate p2 a | Por p1 p2 => sat_predicate p1 a || sat_predicate p2 a @@ -152,7 +164,9 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := | O => None | S n => match p with - | Pvar p' => Some (((true, p') :: nil) :: nil) + | Pvar p' => Some (((true, Pos.to_nat p') :: nil) :: nil) + | Ptrue => Some nil + | Pfalse => Some (nil::nil) | Pand p1 p2 => match trans_pred_temp n p1, trans_pred_temp n p2 with | Some p1', Some p2' => @@ -165,7 +179,9 @@ Fixpoint trans_pred_temp (bound: nat) (p: pred_op) : option formula := Some (mult p1' p2') | _, _ => None end - | Pnot (Pvar p') => Some (((false, p') :: nil) :: nil) + | Pnot Pfalse => Some nil + | Pnot Ptrue => Some (nil::nil) + | Pnot (Pvar p') => Some (((false, Pos.to_nat p') :: nil) :: nil) | Pnot (Pnot p) => trans_pred_temp n p | Pnot (Pand p1 p2) => trans_pred_temp n (Por (Pnot p1) (Pnot p2)) | Pnot (Por p1 p2) => trans_pred_temp n (Pand (Pnot p1) (Pnot p2)) @@ -180,7 +196,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | O => None | S n => match p with - | Pvar p' => Some (exist _ (((true, p') :: nil) :: nil) _) + | Pvar p' => Some (exist _ (((true, Pos.to_nat p') :: nil) :: nil) _) + | Ptrue => Some (exist _ nil _) + | Pfalse => Some (exist _ (nil::nil) _) | Pand p1 p2 => match trans_pred n p1, trans_pred n p2 with | Some (exist _ p1' _), Some (exist _ p2' _) => @@ -193,7 +211,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : Some (exist _ (mult p1' p2') _) | _, _ => None end - | Pnot (Pvar p') => Some (exist _ (((false, p') :: nil) :: nil) _) + | Pnot (Pvar p') => Some (exist _ (((false, Pos.to_nat p') :: nil) :: nil) _) + | Pnot Ptrue => Some (exist _ (nil::nil) _) + | Pnot Pfalse => Some (exist _ nil _) | Pnot (Pnot p') => match trans_pred n p' with | Some (exist _ p1' _) => Some (exist _ p1' _) @@ -210,9 +230,9 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : | None => None end end - end); split; intros; simpl in *; auto. + end); split; intros; simpl in *; auto; try solve [crush]. - inv H. inv H0; auto. - - split; auto. destruct (a p') eqn:?; crush. + - split; auto. destruct (a (Pos.to_nat p')) eqn:?; crush. - inv H. inv H0. unfold satLit in H. simplify. rewrite H. auto. crush. - rewrite negb_involutive in H. apply i in H. auto. @@ -232,7 +252,7 @@ Fixpoint trans_pred (bound: nat) (p: pred_op) : - apply orb_true_intro. apply satFormula_mult2 in H. inv H. apply i in H0. auto. apply i0 in H0. auto. -Qed. +Defined. Definition sat_pred (bound: nat) (p: pred_op) : option ({al : alist | sat_predicate p (interp_alist al) = true} @@ -251,7 +271,7 @@ Definition sat_pred (bound: nat) (p: pred_op) : - intros. specialize (n a). specialize (i a). destruct (sat_predicate p a). exfalso. apply n. apply i. auto. auto. -Qed. +Defined. Definition sat_pred_simple (bound: nat) (p: pred_op) := match sat_pred bound p with @@ -331,6 +351,17 @@ Fixpoint max_reg_cfi (m : positive) (i : cf_instr) := end. Definition regset := Regmap.t val. +Definition predset := PMap.t bool. + +Fixpoint eval_predf (pr: predset) (p: pred_op) {struct p} := + match p with + | Pvar p' => PMap.get p' pr + | Ptrue => true + | Pfalse => false + | Pnot p' => negb (eval_predf pr p') + | Pand p' p'' => (eval_predf pr p') && (eval_predf pr p'') + | Por p' p'' => (eval_predf pr p') || (eval_predf pr p'') + end. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := match rl, vl with @@ -338,11 +369,11 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := | _, _ => Regmap.init Vundef end. -Inductive instr_state : Type := -| InstrState: - forall (rs: regset) - (m: mem), - instr_state. +Record instr_state := mk_instr_state { + is_rs: regset; + is_ps: predset; + is_mem: mem; +}. Section DEFINITION. @@ -379,7 +410,8 @@ Section DEFINITION. (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (pc: node) (**r program point in calling function *) - (rs: regset), (**r register state in calling function *) + (rs: regset) (**r register state in calling function *) + (pr: predset), (**r predicate state of the calling function *) stackframe. Inductive state : Type := @@ -389,6 +421,7 @@ Section DEFINITION. (sp: val) (**r stack pointer *) (pc: node) (**r current program point in [c] *) (rs: regset) (**r register state *) + (pr: predset) (**r predicate register state *) (m: mem), (**r memory state *) state | Callstate: @@ -424,67 +457,89 @@ Section RELSEM. end end. + Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop := + | eval_pred_true: + forall (pr: predset) p rs pr m i, + eval_predf pr p = true -> + eval_pred (Some p) (mk_instr_state rs pr m) i i + | eval_pred_false: + forall (pr: predset) p rs pr m i, + eval_predf pr p = false -> + eval_pred (Some p) (mk_instr_state rs pr m) i (mk_instr_state rs pr m) + | eval_pred_none: + forall i i', + eval_pred None i i' i. + Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop := | exec_RBnop: - forall rs m sp, - step_instr sp (InstrState rs m) RBnop (InstrState rs m) + forall sp ist, + step_instr sp ist RBnop ist | exec_RBop: - forall op v res args rs m sp p, - eval_operation ge sp op rs##args m = Some v -> - step_instr sp (InstrState rs m) - (RBop p op args res) - (InstrState (rs#res <- v) m) + forall op v res args rs m sp p ist pr, + eval_operation ge sp op rs##args m = Some v -> + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#res <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBop p op args res) ist | exec_RBload: - forall addr rs args a chunk m v dst sp p, - eval_addressing ge sp addr rs##args = Some a -> - Mem.loadv chunk m a = Some v -> - step_instr sp (InstrState rs m) - (RBload p chunk addr args dst) - (InstrState (rs#dst <- v) m) + forall addr rs args a chunk m v dst sp p pr ist, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + eval_pred p (mk_instr_state rs pr m) (mk_instr_state (rs#dst <- v) pr m) ist -> + step_instr sp (mk_instr_state rs pr m) (RBload p chunk addr args dst) ist | exec_RBstore: - forall addr rs args a chunk m src m' sp p, - eval_addressing ge sp addr rs##args = Some a -> - Mem.storev chunk m a rs#src = Some m' -> - step_instr sp (InstrState rs m) - (RBstore p chunk addr args src) - (InstrState rs m'). + forall addr rs args a chunk m src m' sp p pr ist, + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a rs#src = Some m' -> + eval_pred p (mk_instr_state rs pr m) (mk_instr_state rs pr m') ist -> + step_instr sp (mk_instr_state rs pr m) (RBstore p chunk addr args src) ist + | exec_RBsetpred: + forall sp rs pr m p c b args, + Op.eval_condition c rs##args m = Some b -> + step_instr sp (mk_instr_state rs pr m) (RBsetpred c args p) + (mk_instr_state rs (PMap.set p b pr) m). Inductive step_cf_instr: state -> cf_instr -> trace -> state -> Prop := | exec_RBcall: - forall s f sp rs m res fd ros sig args pc pc', + forall s f sp rs m res fd ros sig args pc pc' pr, find_function ros rs = Some fd -> funsig fd = sig -> - step_cf_instr (State s f sp pc rs m) (RBcall sig ros args res pc') - E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m) + step_cf_instr (State s f sp pc rs pr m) (RBcall sig ros args res pc') + E0 (Callstate (Stackframe res f sp pc' rs pr :: s) fd rs##args m) | exec_RBtailcall: - forall s f stk rs m sig ros args fd m' pc, + forall s f stk rs m sig ros args fd m' pc pr, find_function ros rs = Some fd -> funsig fd = sig -> Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBtailcall sig ros args) + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBtailcall sig ros args) E0 (Callstate s fd rs##args m') | exec_RBbuiltin: - forall s f sp rs m ef args res pc' vargs t vres m' pc, + forall s f sp rs m ef args res pc' vargs t vres m' pc pr, eval_builtin_args ge (fun r => rs#r) sp m args vargs -> external_call ef ge vargs m t vres m' -> - step_cf_instr (State s f sp pc rs m) (RBbuiltin ef args res pc') - t (State s f sp pc' (regmap_setres res vres rs) m') + step_cf_instr (State s f sp pc rs pr m) (RBbuiltin ef args res pc') + t (State s f sp pc' (regmap_setres res vres rs) pr m') | exec_RBcond: - forall s f sp rs m cond args ifso ifnot b pc pc', + forall s f sp rs m cond args ifso ifnot b pc pc' pr, eval_condition cond rs##args m = Some b -> pc' = (if b then ifso else ifnot) -> - step_cf_instr (State s f sp pc rs m) (RBcond cond args ifso ifnot) - E0 (State s f sp pc' rs m) + step_cf_instr (State s f sp pc rs pr m) (RBcond cond args ifso ifnot) + E0 (State s f sp pc' rs pr m) | exec_RBjumptable: - forall s f sp rs m arg tbl n pc pc', + forall s f sp rs m arg tbl n pc pc' pr, rs#arg = Vint n -> list_nth_z tbl (Int.unsigned n) = Some pc' -> - step_cf_instr (State s f sp pc rs m) (RBjumptable arg tbl) - E0 (State s f sp pc' rs m) - | exec_Ireturn: - forall s f stk rs m or pc m', + step_cf_instr (State s f sp pc rs pr m) (RBjumptable arg tbl) + E0 (State s f sp pc' rs pr m) + | exec_RBreturn: + forall s f stk rs m or pc m' pr, Mem.free m stk 0 f.(fn_stacksize) = Some m' -> - step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs m) (RBreturn or) - E0 (Returnstate s (regmap_optget or Vundef rs) m'). + step_cf_instr (State s f (Vptr stk Ptrofs.zero) pc rs pr m) (RBreturn or) + E0 (Returnstate s (regmap_optget or Vundef rs) m') + | exec_RBgoto: + forall s f sp pc rs pr m pc', + step_cf_instr (State s f sp pc rs pr m) (RBgoto pc') E0 (State s f sp pc' rs pr m) + | exec_RBpred_cf: + forall s f sp pc rs pr m cf1 cf2 st' p t, + step_cf_instr (State s f sp pc rs pr m) (if eval_predf pr p then cf1 else cf2) t st' -> + step_cf_instr (State s f sp pc rs pr m) (RBpred_cf p cf1 cf2) t st'. End RELSEM. diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v index 2e78d36..4986cff 100644 --- a/src/hls/RTLPar.v +++ b/src/hls/RTLPar.v @@ -80,11 +80,11 @@ Section RELSEM. Inductive step: state -> trace -> state -> Prop := | exec_bblock: - forall s f sp pc rs rs' m m' t s' bb, + forall s f sp pc rs rs' m m' t s' bb pr pr', f.(fn_code)!pc = Some bb -> - step_instr_block sp (InstrState rs m) bb.(bb_body) (InstrState rs' m') -> - step_cf_instr ge (State s f sp pc rs' m') bb.(bb_exit) t s' -> - step (State s f sp pc rs m) t s' + step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') -> + step_cf_instr ge (State s f sp pc rs' pr' m') bb.(bb_exit) t s' -> + step (State s f sp pc rs pr m) t s' | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -94,6 +94,7 @@ Section RELSEM. (Vptr stk Ptrofs.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) + (PMap.init false) m') | exec_function_external: forall s ef args res t m m', @@ -101,9 +102,9 @@ Section RELSEM. step (Callstate s (External ef) args m) t (Returnstate s res m') | exec_return: - forall res f sp pc rs s vres m, - step (Returnstate (Stackframe res f sp pc rs :: s) vres m) - E0 (State s f sp pc (rs#res <- vres) m). + forall res f sp pc rs s vres m pr, + step (Returnstate (Stackframe res f sp pc rs pr :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) pr m). End RELSEM. diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v index 5ad3f90..13d9480 100644 --- a/src/hls/RTLPargen.v +++ b/src/hls/RTLPargen.v @@ -19,7 +19,7 @@ Require Import compcert.backend.Registers. Require Import compcert.common.AST. Require Import compcert.common.Globalenvs. -Require compcert.common.Memory. +Require Import compcert.common.Memory. Require Import compcert.common.Values. Require Import compcert.lib.Floats. Require Import compcert.lib.Integers. @@ -30,469 +30,154 @@ Require Import vericert.common.Vericertlib. Require Import vericert.hls.RTLBlock. Require Import vericert.hls.RTLPar. Require Import vericert.hls.RTLBlockInstr. - -(*| -Schedule Oracle -=============== - -This oracle determines if a schedule was valid by performing symbolic execution on the input and -output and showing that these behave the same. This acts on each basic block separately, as the -rest of the functions should be equivalent. -|*) - -Definition reg := positive. - -Inductive resource : Set := -| Reg : reg -> resource -| Mem : resource. - -(*| -The following defines quite a few equality comparisons automatically, however, these can be -optimised heavily if written manually, as their proofs are not needed. -|*) - -Lemma resource_eq : forall (r1 r2 : resource), {r1 = r2} + {r1 <> r2}. -Proof. - decide equality. apply Pos.eq_dec. -Defined. - -Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma condition_eq: forall (x y : Op.condition), {x = y} + {x <> y}. -Proof. - generalize comparison_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - decide equality. -Defined. - -Lemma addressing_eq : forall (x y : Op.addressing), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize Z.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - decide equality. -Defined. - -Lemma typ_eq : forall (x y : AST.typ), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma operation_eq: forall (x y : Op.operation), {x = y} + {x <> y}. -Proof. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize AST.ident_eq; intro. - generalize condition_eq; intro. - generalize addressing_eq; intro. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma memory_chunk_eq : forall (x y : AST.memory_chunk), {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -Lemma list_typ_eq: forall (x y : list AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma option_typ_eq : forall (x y : option AST.typ), {x = y} + {x <> y}. -Proof. - generalize typ_eq; intro. - decide equality. -Defined. - -Lemma signature_eq: forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma list_operation_eq : forall (x y : list Op.operation), {x = y} + {x <> y}. -Proof. - generalize operation_eq; intro. - decide equality. -Defined. - -Lemma list_reg_eq : forall (x y : list reg), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intros. - decide equality. -Defined. - -Lemma sig_eq : forall (x y : AST.signature), {x = y} + {x <> y}. -Proof. - repeat decide equality. -Defined. - -Lemma instr_eq: forall (x y : instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -Lemma cf_instr_eq: forall (x y : cf_instr), {x = y} + {x <> y}. -Proof. - generalize Pos.eq_dec; intro. - generalize typ_eq; intro. - generalize Int.eq_dec; intro. - generalize Int64.eq_dec; intro. - generalize Float.eq_dec; intro. - generalize Float32.eq_dec; intro. - generalize Ptrofs.eq_dec; intro. - generalize memory_chunk_eq; intro. - generalize addressing_eq; intro. - generalize operation_eq; intro. - generalize condition_eq; intro. - generalize signature_eq; intro. - generalize list_operation_eq; intro. - generalize list_reg_eq; intro. - generalize AST.ident_eq; intro. - repeat decide equality. -Defined. - -(*| -We then create equality lemmas for a resource and a module to index resources uniquely. The -indexing is done by setting Mem to 1, whereas all other infinitely many registers will all be -shifted right by 1. This means that they will never overlap. -|*) - -Module R_indexed. - Definition t := resource. - Definition index (rs: resource) : positive := - match rs with - | Reg r => xO r - | Mem => 1%positive - end. - - Lemma index_inj: forall (x y: t), index x = index y -> x = y. - Proof. destruct x; destruct y; crush. Qed. - - Definition eq := resource_eq. -End R_indexed. - -(*| -We can then create expressions that mimic the expressions defined in RTLBlock and RTLPar, which use -expressions instead of registers as their inputs and outputs. This means that we can accumulate all -the results of the operations as general expressions that will be present in those registers. - -- Ebase: the starting value of the register. -- Eop: Some arithmetic operation on a number of registers. -- Eload: A load from a memory location into a register. -- Estore: A store from a register to a memory location. - -Then, to make recursion over expressions easier, expression_list is also defined in the datatype, as -that enables mutual recursive definitions over the datatypes. -|*) - -Inductive expression : Set := -| Ebase : resource -> expression -| Eop : Op.operation -> expression_list -> expression -| Eload : AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -| Estore : expression -> AST.memory_chunk -> Op.addressing -> expression_list -> expression -> expression -with expression_list : Set := -| Enil : expression_list -| Econs : expression -> expression_list -> expression_list. - -(*| -Using IMap we can create a map from resources to any other type, as resources can be uniquely -identified as positive numbers. -|*) - -Module Rtree := ITree(R_indexed). - -Definition forest : Type := Rtree.t expression. - -Definition regset := Registers.Regmap.t val. - -Definition get_forest v f := - match Rtree.get v f with - | None => Ebase v - | Some v' => v' +Require Import vericert.hls.Abstr. + +#[local] Open Scope positive. +#[local] Open Scope forest. + +(*Parameter op_le : Op.operation -> Op.operation -> bool. +Parameter chunk_le : AST.memory_chunk -> AST.memory_chunk -> bool. +Parameter addr_le : Op.addressing -> Op.addressing -> bool. +Parameter cond_le : Op.condition -> Op.condition -> bool. + +Fixpoint pred_le (p1 p2: pred_op) : bool := + match p1, p2 with + | Pvar i, Pvar j => (i <=? j)%positive + | Pnot p1, Pnot p2 => pred_le p1 p2 + | Pand p1 p1', Pand p2 p2' => if pred_le p1 p2 then true else pred_le p1' p2' + | Por p1 p1', Por p2 p2' => if pred_le p1 p2 then true else pred_le p1' p2' + | Pvar _, _ => true + | Pnot _, Pvar _ => false + | Pnot _, _ => true + | Pand _ _, Pvar _ => false + | Pand _ _, Pnot _ => false + | Pand _ _, _ => true + | Por _ _, _ => false end. -Notation "a # b" := (get_forest b a) (at level 1). -Notation "a # b <- c" := (Rtree.set b c a) (at level 1, b at next level). +Import Lia. -Record sem_state := mk_sem_state { - sem_state_regset : regset; - sem_state_memory : Memory.mem - }. +Lemma pred_le_trans : + forall p1 p2 p3 b, pred_le p1 p2 = b -> pred_le p2 p3 = b -> pred_le p1 p3 = b. +Proof. + induction p1; destruct p2; destruct p3; crush. + destruct b. rewrite Pos.leb_le in *. lia. rewrite Pos.leb_gt in *. lia. + firstorder. + destruct (pred_le p1_1 p2_1) eqn:?. subst. destruct (pred_le p2_1 p3_1) eqn:?. + apply IHp1_1 in Heqb. rewrite Heqb. auto. auto. -(*| -Finally we want to define the semantics of execution for the expressions with symbolic values, so -the result of executing the expressions will be an expressions. -|*) -Section SEMANTICS. - -Context (A : Set) (genv : Genv.t A unit). - -Inductive sem_value : - val -> sem_state -> expression -> val -> Prop := - | Sbase_reg: - forall sp st r, - sem_value sp st (Ebase (Reg r)) (Registers.Regmap.get r (sem_state_regset st)) - | Sop: - forall st op args v lv sp, - sem_val_list sp st args lv -> - Op.eval_operation genv sp op lv (sem_state_memory st) = Some v -> - sem_value sp st (Eop op args) v - | Sload : - forall st mem_exp addr chunk args a v m' lv sp, - sem_mem sp st mem_exp m' -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.loadv chunk m' a = Some v -> - sem_value sp st (Eload chunk addr args mem_exp) v -with sem_mem : - val -> sem_state -> expression -> Memory.mem -> Prop := - | Sstore : - forall st mem_exp val_exp m'' addr v a m' chunk args lv sp, - sem_mem sp st mem_exp m' -> - sem_value sp st val_exp v -> - sem_val_list sp st args lv -> - Op.eval_addressing genv sp addr lv = Some a -> - Memory.Mem.storev chunk m' a v = Some m'' -> - sem_mem sp st (Estore mem_exp chunk addr args val_exp) m'' - | Sbase_mem : - forall st m sp, - sem_mem sp st (Ebase Mem) m -with sem_val_list : - val -> sem_state -> expression_list -> list val -> Prop := - | Snil : - forall st sp, - sem_val_list sp st Enil nil - | Scons : - forall st e v l lv sp, - sem_value sp st e v -> - sem_val_list sp st l lv -> - sem_val_list sp st (Econs e l) (v :: lv). - -Inductive sem_regset : - val -> sem_state -> forest -> regset -> Prop := - | Sregset: - forall st f rs' sp, - (forall x, sem_value sp st (f # (Reg x)) (Registers.Regmap.get x rs')) -> - sem_regset sp st f rs'. - -Inductive sem : - val -> sem_state -> forest -> sem_state -> Prop := - | Sem: - forall st rs' m' f sp, - sem_regset sp st f rs' -> - sem_mem sp st (f # Mem) m' -> - sem sp st f (mk_sem_state rs' m'). - -End SEMANTICS. - -Fixpoint beq_expression (e1 e2: expression) {struct e1}: bool := +Fixpoint expr_le (e1 e2: expression) {struct e2}: bool := match e1, e2 with - | Ebase r1, Ebase r2 => if resource_eq r1 r2 then true else false - | Eop op1 el1, Eop op2 el2 => - if operation_eq op1 op2 then beq_expression_list el1 el2 else false - | Eload chk1 addr1 el1 e1, Eload chk2 addr2 el2 e2 => - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then beq_expression e1 e2 else false else false else false - | Estore m1 chk1 addr1 el1 e1, Estore m2 chk2 addr2 el2 e2=> - if memory_chunk_eq chk1 chk2 - then if addressing_eq addr1 addr2 - then if beq_expression_list el1 el2 - then if beq_expression m1 m2 - then beq_expression e1 e2 else false else false else false else false - | _, _ => false + | Ebase r1, Ebase r2 => (R_indexed.index r1 <=? R_indexed.index r2)%positive + | Ebase _, _ => true + | Eop op1 elist1 m1, Eop op2 elist2 m2 => + if op_le op1 op2 then true + else if elist_le elist1 elist2 then true + else expr_le m1 m2 + | Eop _ _ _, Ebase _ => false + | Eop _ _ _, _ => true + | Eload chunk1 addr1 elist1 expr1, Eload chunk2 addr2 elist2 expr2 => + if chunk_le chunk1 chunk2 then true + else if addr_le addr1 addr2 then true + else if elist_le elist1 elist2 then true + else expr_le expr1 expr2 + | Eload _ _ _ _, Ebase _ => false + | Eload _ _ _ _, Eop _ _ _ => false + | Eload _ _ _ _, _ => true + | Estore m1 chunk1 addr1 elist1 expr1, Estore m2 chunk2 addr2 elist2 expr2 => + if expr_le m1 m2 then true + else if chunk_le chunk1 chunk2 then true + else if addr_le addr1 addr2 then true + else if elist_le elist1 elist2 then true + else expr_le expr1 expr2 + | Estore _ _ _ _ _, Ebase _ => false + | Estore _ _ _ _ _, Eop _ _ _ => false + | Estore _ _ _ _ _, Eload _ _ _ _ => false + | Estore _ _ _ _ _, _ => true + | Esetpred p1 cond1 elist1 m1, Esetpred p2 cond2 elist2 m2 => + if (p1 <=? p2)%positive then true + else if cond_le cond1 cond2 then true + else if elist_le elist1 elist2 then true + else expr_le m1 m2 + | Esetpred _ _ _ _, Econd _ => true + | Esetpred _ _ _ _, _ => false + | Econd eplist1, Econd eplist2 => eplist_le eplist1 eplist2 + | Econd eplist1, _ => false end -with beq_expression_list (el1 el2: expression_list) {struct el1} : bool := - match el1, el2 with +with elist_le (e1 e2: expression_list) : bool := + match e1, e2 with | Enil, Enil => true - | Econs e1 t1, Econs e2 t2 => beq_expression e1 e2 && beq_expression_list t1 t2 - | _, _ => false - end. - -Scheme expression_ind2 := Induction for expression Sort Prop - with expression_list_ind2 := Induction for expression_list Sort Prop. - -Lemma beq_expression_correct: - forall e1 e2, beq_expression e1 e2 = true -> e1 = e2. -Proof. - intro e1; - apply expression_ind2 with - (P := fun (e1 : expression) => - forall e2, beq_expression e1 e2 = true -> e1 = e2) - (P0 := fun (e1 : expression_list) => - forall e2, beq_expression_list e1 e2 = true -> e1 = e2); simplify; - repeat match goal with - | [ H : context[match ?x with _ => _ end] |- _ ] => destruct x eqn:? - | [ H : context[if ?x then _ else _] |- _ ] => destruct x eqn:? - end; subst; f_equal; crush. -Qed. - -Definition empty : forest := Rtree.empty _. - -(*| -This function checks if all the elements in [fa] are in [fb], but not the other way round. -|*) - -Definition check := Rtree.beq beq_expression. - -Lemma check_correct: forall (fa fb : forest) (x : resource), - check fa fb = true -> (forall x, fa # x = fb # x). -Proof. - unfold check, get_forest; intros; - pose proof beq_expression_correct; - match goal with - [ Hbeq : context[Rtree.beq], y : Rtree.elt |- _ ] => - apply (Rtree.beq_sound beq_expression fa fb) with (x := y) in Hbeq - end; - repeat destruct_match; crush. -Qed. - -Lemma get_empty: - forall r, empty#r = Ebase r. -Proof. - intros; unfold get_forest; - destruct_match; auto; [ ]; - match goal with - [ H : context[Rtree.get _ empty] |- _ ] => rewrite Rtree.gempty in H - end; discriminate. -Qed. - -Fixpoint beq2 {A B : Type} (beqA : A -> B -> bool) (m1 : PTree.t A) (m2 : PTree.t B) {struct m1} : bool := - match m1, m2 with - | PTree.Leaf, _ => PTree.bempty m2 - | _, PTree.Leaf => PTree.bempty m1 - | PTree.Node l1 o1 r1, PTree.Node l2 o2 r2 => - match o1, o2 with - | None, None => true - | Some y1, Some y2 => beqA y1 y2 - | _, _ => false - end - && beq2 beqA l1 l2 && beq2 beqA r1 r2 - end. - -Lemma beq2_correct: - forall A B beqA m1 m2, - @beq2 A B beqA m1 m2 = true <-> - (forall (x: PTree.elt), - match PTree.get x m1, PTree.get x m2 with - | None, None => True - | Some y1, Some y2 => beqA y1 y2 = true - | _, _ => False - end). -Proof. - induction m1; intros. - - simpl. rewrite PTree.bempty_correct. split; intros. - rewrite PTree.gleaf. rewrite H. auto. - generalize (H x). rewrite PTree.gleaf. destruct (PTree.get x m2); tauto. - - destruct m2. - + unfold beq2. rewrite PTree.bempty_correct. split; intros. - rewrite H. rewrite PTree.gleaf. auto. - generalize (H x). rewrite PTree.gleaf. - destruct (PTree.get x (PTree.Node m1_1 o m1_2)); tauto. - + simpl. split; intros. - * destruct (andb_prop _ _ H). destruct (andb_prop _ _ H0). - rewrite IHm1_1 in H3. rewrite IHm1_2 in H1. - destruct x; simpl. apply H1. apply H3. - destruct o; destruct o0; auto || congruence. - * apply andb_true_intro. split. apply andb_true_intro. split. - generalize (H xH); simpl. destruct o; destruct o0; tauto. - apply IHm1_1. intros; apply (H (xO x)). - apply IHm1_2. intros; apply (H (xI x)). -Qed. - -Lemma map0: - forall r, - empty # r = Ebase r. -Proof. intros; eapply get_empty. Qed. - -Lemma map1: - forall w dst dst', - dst <> dst' -> - (empty # dst <- w) # dst' = Ebase dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto; apply map0. Qed. - -Lemma genmap1: - forall (f : forest) w dst dst', - dst <> dst' -> - (f # dst <- w) # dst' = f # dst'. -Proof. intros; unfold get_forest; rewrite Rtree.gso; auto. Qed. - -Lemma map2: - forall (v : expression) x rs, - (rs # x <- v) # x = v. -Proof. intros; unfold get_forest; rewrite Rtree.gss; trivial. Qed. - -Lemma tri1: - forall x y, - Reg x <> Reg y -> x <> y. -Proof. crush. Qed. + | Econs a1 b1, Econs a2 b2 => if expr_le a1 a2 then true else elist_le b1 b2 + | Enil, _ => true + | _, Enil => false + end +with eplist_le (e1 e2: expr_pred_list) : bool := + match e1, e2 with + | EPnil, EPnil => true + | EPcons p1 a1 b1, EPcons p2 a2 b2 => + if pred_le p1 p2 then true + else if expr_le a1 a2 then true else eplist_le b1 b2 + | EPnil, _ => true + | _, EPnil => false + end +.*) Definition ge_preserved {A B C D: Type} (ge: Genv.t A B) (tge: Genv.t C D) : Prop := - (forall sp op vl, Op.eval_operation ge sp op vl = - Op.eval_operation tge sp op vl) + (forall sp op vl m, Op.eval_operation ge sp op vl m = + Op.eval_operation tge sp op vl m) /\ (forall sp addr vl, Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl). Lemma ge_preserved_same: forall A B ge, @ge_preserved A B A B ge ge. Proof. unfold ge_preserved; auto. Qed. -Hint Resolve ge_preserved_same : rtlpar. +#[local] Hint Resolve ge_preserved_same : rtlpar. -Inductive sem_state_ld : sem_state -> sem_state -> Prop := -| sem_state_ld_intro: - forall rs rs' m m', - regs_lessdef rs rs' -> +Ltac rtlpar_crush := crush; eauto with rtlpar. + +Inductive match_states : instr_state -> instr_state -> Prop := +| match_states_intro: + forall ps ps' rs rs' m m', + (forall x, rs !! x = rs' !! x) -> + (forall x, ps !! x = ps' !! x) -> m = m' -> - sem_state_ld (mk_sem_state rs m) (mk_sem_state rs' m'). + match_states (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). + +Inductive match_states_ld : instr_state -> instr_state -> Prop := +| match_states_ld_intro: + forall ps ps' rs rs' m m', + regs_lessdef rs rs' -> + (forall x, ps !! x = ps' !! x) -> + Mem.extends m m' -> + match_states_ld (mk_instr_state rs ps m) (mk_instr_state rs' ps' m'). Lemma sems_det: - forall A ge tge sp st f, + forall A ge tge sp f rs ps m, ge_preserved ge tge -> forall v v' mv mv', - (sem_value A ge sp st f v /\ sem_value A tge sp st f v' -> v = v') /\ - (sem_mem A ge sp st f mv /\ sem_mem A tge sp st f mv' -> mv = mv'). + (@sem_value A (mk_ctx rs ps m sp ge) f v /\ @sem_value A (mk_ctx rs ps m sp tge) f v' -> v = v') /\ + (@sem_mem A (mk_ctx rs ps m sp ge) f mv /\ @sem_mem A (mk_ctx rs ps m sp tge) f mv' -> mv = mv'). Proof. Abort. (*Lemma sem_value_det: forall A ge tge sp st f v v', ge_preserved ge tge -> - sem_value A ge sp st f v -> - sem_value A tge sp st f v' -> + @sem_value A ge sp st f v -> + @sem_value A tge sp st f v' -> v = v'. Proof. - intros; - generalize (sems_det A ge tge sp st f H v v' - st.(sem_state_memory) st.(sem_state_memory)); + intros. destruct st. + generalize (sems_det A ge tge sp (mk_instr_state rs m) f H v v' + m m); crush. Qed. Hint Resolve sem_value_det : rtlpar. Lemma sem_value_det': forall FF ge sp s f v v', - sem_value FF ge sp s f v -> - sem_value FF ge sp s f v' -> + @sem_value FF ge sp s f v -> + @sem_value FF ge sp s f v' -> v = v'. Proof. simplify; eauto with rtlpar. @@ -501,20 +186,20 @@ Qed. Lemma sem_mem_det: forall A ge tge sp st f m m', ge_preserved ge tge -> - sem_mem A ge sp st f m -> - sem_mem A tge sp st f m' -> + @sem_mem A ge sp st f m -> + @sem_mem A tge sp st f m' -> m = m'. Proof. - intros; - generalize (sems_det A ge tge sp st f H sp sp m m'); + intros. destruct st. + generalize (sems_det A ge tge sp (mk_instr_state rs m0) f H sp sp m m'); crush. Qed. Hint Resolve sem_mem_det : rtlpar. Lemma sem_mem_det': forall FF ge sp s f m m', - sem_mem FF ge sp s f m -> - sem_mem FF ge sp s f m' -> + @sem_mem FF ge sp s f m -> + @sem_mem FF ge sp s f m' -> m = m'. Proof. simplify; eauto with rtlpar. @@ -525,9 +210,9 @@ Hint Resolve Val.lessdef_same : rtlpar. Lemma sem_regset_det: forall FF ge tge sp st f v v', ge_preserved ge tge -> - sem_regset FF ge sp st f v -> - sem_regset FF tge sp st f v' -> - regs_lessdef v v'. + @sem_regset FF ge sp st f v -> + @sem_regset FF tge sp st f v' -> + (forall x, v !! x = v' !! x). Proof. intros; unfold regs_lessdef. inv H0; inv H1; @@ -538,9 +223,9 @@ Hint Resolve sem_regset_det : rtlpar. Lemma sem_det: forall FF ge tge sp st f st' st'', ge_preserved ge tge -> - sem FF ge sp st f st' -> - sem FF tge sp st f st'' -> - sem_state_ld st' st''. + @sem FF ge sp st f st' -> + @sem FF tge sp st f st'' -> + match_states st' st''. Proof. intros. destruct st; destruct st'; destruct st''. @@ -551,30 +236,117 @@ Hint Resolve sem_det : rtlpar. Lemma sem_det': forall FF ge sp st f st' st'', - sem FF ge sp st f st' -> - sem FF ge sp st f st'' -> - sem_state_ld st' st''. + @sem FF ge sp st f st' -> + @sem FF ge sp st f st'' -> + match_states st' st''. Proof. eauto with rtlpar. Qed. (*| Update functions. |*) +*) -Fixpoint list_translation (l : list reg) (f : forest) {struct l} : expression_list := +Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr := match l with - | nil => Enil - | i :: l => Econs (f # (Reg i)) (list_translation l f) + | nil => nil + | i :: l => (f # (Reg i)) :: (list_translation l f) + end. + +Fixpoint replicate {A} (n: nat) (l: A) := + match n with + | O => nil + | S n => l :: replicate n l + end. + +Definition merge''' x y := + match x, y with + | Some p1, Some p2 => Some (Pand p1 p2) + | Some p, None | None, Some p => Some p + | None, None => None + end. + +Definition merge'' x := + match x with + | ((a, e), (b, el)) => (merge''' a b, Econs e el) + end. + +Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) := + match p1, p2 with + | Psingle a, Psingle b => Psingle (a, b) + | Psingle a, Plist b => Plist (NE.map (fun x => (fst x, (a, snd x))) b) + | Plist b, Psingle a => Plist (NE.map (fun x => (fst x, (snd x, a))) b) + | Plist a, Plist b => + Plist (NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end) + (NE.non_empty_prod a b)) + end. + +Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B := + match p with + | Psingle a => Psingle (f a) + | Plist b => Plist (NE.map (fun x => (fst x, f (snd x))) b) + end. + +(*map (fun x => (fst x, Econs (snd x) Enil)) pel*) +Definition merge' (pel: pred_expr) (tpel: predicated expression_list) := + predicated_map (uncurry Econs) (predicated_prod pel tpel). + +Fixpoint merge (pel: list pred_expr): predicated expression_list := + match pel with + | nil => Psingle Enil + | a :: b => merge' a (merge b) + end. + +Definition map_pred_op {A B} (pf: option pred_op * (A -> B)) (pa: option pred_op * A): option pred_op * B := + match pa, pf with + | (p, a), (p', f) => (merge''' p p', f a) + end. + +Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): predicated B := + predicated_map (fun x => (fst x) (snd x)) (predicated_prod pf pa). + +Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A): predicated B := + match pf with + | Psingle f => Psingle (f pa) + | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa)) pf') + end. + +Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C := + match pf with + | Psingle f => Psingle (f pa pb) + | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb)) pf') + end. + +Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D := + match pf with + | Psingle f => Psingle (f pa pb pc) + | Plist pf' => Plist (NE.map (fun x => (fst x, (snd x) pa pb pc)) pf') + end. + +(*Compute merge (((Some (Pvar 2), Ebase (Reg 4))::nil)::((Some (Pvar 3), Ebase (Reg 3))::(Some (Pvar 1), Ebase (Reg 3))::nil)::nil).*) + +Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) := + match p with + | None => Psingle a + | Some x => Plist (NE.singleton (x, a)) end. Definition update (f : forest) (i : instr) : forest := match i with | RBnop => f | RBop p op rl r => - f # (Reg r) <- (Eop op (list_translation rl f)) + f # (Reg r) <- + (map_predicated (predicated_from_opt p (Eop op)) (merge (list_translation rl f))) | RBload p chunk addr rl r => - f # (Reg r) <- (Eload chunk addr (list_translation rl f) (f # Mem)) + f # (Reg r) <- + (map_predicated + (map_predicated (predicated_from_opt p (Eload chunk addr)) (merge (list_translation rl f))) + (f # Mem)) | RBstore p chunk addr rl r => - f # Mem <- (Estore (f # Mem) chunk addr (list_translation rl f) (f # (Reg r))) + f # Mem <- + (map_predicated + (map_predicated + (predicated_apply2 (map_predicated (predicated_from_opt p Estore) (f # (Reg r))) chunk addr) + (merge (list_translation rl f))) (f # Mem)) | RBsetpred c addr p => f end. @@ -588,7 +360,7 @@ Get a sequence from the basic block. Fixpoint abstract_sequence (f : forest) (b : list instr) : forest := match b with | nil => f - | i :: l => update (abstract_sequence f l) i + | i :: l => abstract_sequence (update f i) l end. (*| @@ -650,14 +422,685 @@ Abstract computations ===================== |*) +(*Definition is_regs i := match i with mk_instr_state rs _ => rs end. +Definition is_mem i := match i with mk_instr_state _ m => m end. + +Inductive state_lessdef : instr_state -> instr_state -> Prop := + state_lessdef_intro : + forall rs1 rs2 m1, + (forall x, rs1 !! x = rs2 !! x) -> + state_lessdef (mk_instr_state rs1 m1) (mk_instr_state rs2 m1). + +(*| +RTLBlock to abstract translation +-------------------------------- + +Correctness of translation from RTLBlock to the abstract interpretation language. +|*) + +Lemma match_states_refl x : match_states x x. +Proof. destruct x; constructor; crush. Qed. + +Lemma match_states_commut x y : match_states x y -> match_states y x. +Proof. inversion 1; constructor; crush. Qed. + +Lemma match_states_trans x y z : + match_states x y -> match_states y z -> match_states x z. +Proof. repeat inversion 1; constructor; crush. Qed. + +Ltac inv_simp := + repeat match goal with + | H: exists _, _ |- _ => inv H + end; simplify. + +Lemma abstract_interp_empty A ge sp st : @sem A ge sp st empty st. +Proof. destruct st; repeat constructor. Qed. + +Lemma abstract_interp_empty3 : + forall A ge sp st st', + @sem A ge sp st empty st' -> + match_states st st'. +Proof. + inversion 1; subst; simplify. + destruct st. inv H1. simplify. + constructor. unfold regs_lessdef. + intros. inv H0. specialize (H1 x). inv H1; auto. + auto. +Qed.*) + +Definition check_dest i r' := + match i with + | RBop p op rl r => (r =? r')%positive + | RBload p chunk addr rl r => (r =? r')%positive + | _ => false + end. + +Lemma check_dest_dec i r : {check_dest i r = true} + {check_dest i r = false}. +Proof. destruct (check_dest i r); tauto. Qed. + +Fixpoint check_dest_l l r := + match l with + | nil => false + | a :: b => check_dest a r || check_dest_l b r + end. + +Lemma check_dest_l_forall : + forall l r, + check_dest_l l r = false -> + Forall (fun x => check_dest x r = false) l. +Proof. induction l; crush. Qed. + +(*Lemma check_dest_l_ex : + forall l r, + check_dest_l l r = true -> + exists a, In a l /\ check_dest a r = true. +Proof. + induction l; crush. + destruct (check_dest a r) eqn:?; try solve [econstructor; crush]. + simplify. + exploit IHl. apply H. inv_simp. econstructor. simplify. right. eassumption. + auto. +Qed. + +Lemma check_dest_l_dec i r : {check_dest_l i r = true} + {check_dest_l i r = false}. +Proof. destruct (check_dest_l i r); tauto. Qed. + +Lemma check_dest_l_dec2 l r : + {Forall (fun x => check_dest x r = false) l} + + {exists a, In a l /\ check_dest a r = true}. +Proof. + destruct (check_dest_l_dec l r); [right | left]; + auto using check_dest_l_ex, check_dest_l_forall. +Qed. + +Lemma check_dest_l_forall2 : + forall l r, + Forall (fun x => check_dest x r = false) l -> + check_dest_l l r = false. +Proof. + induction l; crush. + inv H. apply orb_false_intro; crush. +Qed. + +Lemma check_dest_l_ex2 : + forall l r, + (exists a, In a l /\ check_dest a r = true) -> + check_dest_l l r = true. +Proof. + induction l; crush. + specialize (IHl r). inv H. + apply orb_true_intro; crush. + apply orb_true_intro; crush. + right. apply IHl. exists x. auto. +Qed. + +Lemma check_dest_update : + forall f i r, + check_dest i r = false -> + (update f i) # (Reg r) = f # (Reg r). +Proof. + destruct i; crush; try apply Pos.eqb_neq in H; apply genmap1; crush. +Qed. + +Lemma check_dest_update2 : + forall f r rl op p, + (update f (RBop p op rl r)) # (Reg r) = Eop op (list_translation rl f) (f # Mem). +Proof. crush; rewrite map2; auto. Qed. + +Lemma check_dest_update3 : + forall f r rl p addr chunk, + (update f (RBload p chunk addr rl r)) # (Reg r) = Eload chunk addr (list_translation rl f) (f # Mem). +Proof. crush; rewrite map2; auto. Qed. + +Lemma abstr_comp : + forall l i f x x0, + abstract_sequence f (l ++ i :: nil) = x -> + abstract_sequence f l = x0 -> + x = update x0 i. +Proof. induction l; intros; crush; eapply IHl; eauto. Qed. + +Lemma abstract_seq : + forall l f i, + abstract_sequence f (l ++ i :: nil) = update (abstract_sequence f l) i. +Proof. induction l; crush. Qed. + +Lemma check_list_l_false : + forall l x r, + check_dest_l (l ++ x :: nil) r = false -> + check_dest_l l r = false /\ check_dest x r = false. +Proof. + simplify. + apply check_dest_l_forall in H. apply Forall_app in H. + simplify. apply check_dest_l_forall2; auto. + apply check_dest_l_forall in H. apply Forall_app in H. + simplify. inv H1. auto. +Qed. + +Lemma check_list_l_true : + forall l x r, + check_dest_l (l ++ x :: nil) r = true -> + check_dest_l l r = true \/ check_dest x r = true. +Proof. + simplify. + apply check_dest_l_ex in H; inv_simp. + apply in_app_or in H. inv H. left. + apply check_dest_l_ex2. exists x0. auto. + inv H0; auto. +Qed. + +Lemma abstract_sequence_update : + forall l r f, + check_dest_l l r = false -> + (abstract_sequence f l) # (Reg r) = f # (Reg r). +Proof. + induction l using rev_ind; crush. + rewrite abstract_seq. rewrite check_dest_update. apply IHl. + apply check_list_l_false in H. tauto. + apply check_list_l_false in H. tauto. +Qed. + +Lemma rtlblock_trans_correct' : + forall bb ge sp st x st'', + RTLBlock.step_instr_list ge sp st (bb ++ x :: nil) st'' -> + exists st', RTLBlock.step_instr_list ge sp st bb st' + /\ step_instr ge sp st' x st''. +Proof. + induction bb. + crush. exists st. + split. constructor. inv H. inv H6. auto. + crush. inv H. exploit IHbb. eassumption. inv_simp. + econstructor. split. + econstructor; eauto. eauto. +Qed. + +Lemma sem_update_RBnop : + forall A ge sp st f st', + @sem A ge sp st f st' -> sem ge sp st (update f RBnop) st'. +Proof. crush. Qed. + +Lemma gen_list_base: + forall FF ge sp l rs exps st1, + (forall x, @sem_value FF ge sp st1 (exps # (Reg x)) (rs !! x)) -> + sem_val_list ge sp st1 (list_translation l exps) rs ## l. +Proof. + induction l. + intros. simpl. constructor. + intros. simpl. eapply Scons; eauto. +Qed. + +Lemma abstract_seq_correct_aux: + forall FF ge sp i st1 st2 st3 f, + @step_instr FF ge sp st3 i st2 -> + sem ge sp st1 f st3 -> + sem ge sp st1 (update f i) st2. +Proof. + intros; inv H; simplify. + { simplify; eauto. } (*apply match_states_refl. }*) + { inv H0. inv H6. destruct st1. econstructor. simplify. + constructor. intros. + destruct (resource_eq (Reg res) (Reg x)). inv e. + rewrite map2. econstructor. eassumption. apply gen_list_base; eauto. + rewrite Regmap.gss. eauto. + assert (res <> x). { unfold not in *. intros. apply n. rewrite H0. auto. } + rewrite Regmap.gso by auto. + rewrite genmap1 by auto. auto. + + rewrite genmap1; crush. } + { inv H0. inv H7. constructor. constructor. intros. + destruct (Pos.eq_dec dst x); subst. + rewrite map2. econstructor; eauto. + apply gen_list_base. auto. rewrite Regmap.gss. auto. + rewrite genmap1. rewrite Regmap.gso by auto. auto. + unfold not in *; intros. inv H0. auto. + rewrite genmap1; crush. + } + { inv H0. inv H7. constructor. constructor; intros. + rewrite genmap1; crush. + rewrite map2. econstructor; eauto. + apply gen_list_base; auto. + } +Qed. + +Lemma regmap_list_equiv : + forall A (rs1: Regmap.t A) rs2, + (forall x, rs1 !! x = rs2 !! x) -> + forall rl, rs1##rl = rs2##rl. +Proof. induction rl; crush. Qed. + +Lemma sem_update_Op : + forall A ge sp st f st' r l o0 o m rs v, + @sem A ge sp st f st' -> + Op.eval_operation ge sp o0 rs ## l m = Some v -> + match_states st' (mk_instr_state rs m) -> + exists tst, + sem ge sp st (update f (RBop o o0 l r)) tst /\ match_states (mk_instr_state (Regmap.set r v rs) m) tst. +Proof. + intros. inv H1. simplify. + destruct st. + econstructor. simplify. + { constructor. + { constructor. intros. destruct (Pos.eq_dec x r); subst. + { pose proof (H5 r). rewrite map2. pose proof H. inv H. econstructor; eauto. + { inv H9. eapply gen_list_base; eauto. } + { instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. erewrite regmap_list_equiv; eauto. } } + { rewrite Regmap.gso by auto. rewrite genmap1; crush. inv H. inv H7; eauto. } } + { inv H. rewrite genmap1; crush. eauto. } } + { constructor; eauto. intros. + destruct (Pos.eq_dec r x); + subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } +Qed. + +Lemma sem_update_load : + forall A ge sp st f st' r o m a l m0 rs v a0, + @sem A ge sp st f st' -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.loadv m m0 a0 = Some v -> + match_states st' (mk_instr_state rs m0) -> + exists tst : instr_state, + sem ge sp st (update f (RBload o m a l r)) tst + /\ match_states (mk_instr_state (Regmap.set r v rs) m0) tst. +Proof. + intros. inv H2. pose proof H. inv H. inv H9. + destruct st. + econstructor; simplify. + { constructor. + { constructor. intros. + destruct (Pos.eq_dec x r); subst. + { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. + rewrite <- H6. eauto. + instantiate (1 := (Regmap.set r v rs0)). rewrite Regmap.gss. auto. } + { rewrite Regmap.gso by auto. rewrite genmap1; crush. } } + { rewrite genmap1; crush. eauto. } } + { constructor; auto; intros. destruct (Pos.eq_dec r x); + subst; [repeat rewrite Regmap.gss | repeat rewrite Regmap.gso]; auto. } +Qed. + +Lemma sem_update_store : + forall A ge sp a0 m a l r o f st m' rs m0 st', + @sem A ge sp st f st' -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.storev m m0 a0 rs !! r = Some m' -> + match_states st' (mk_instr_state rs m0) -> + exists tst, sem ge sp st (update f (RBstore o m a l r)) tst + /\ match_states (mk_instr_state rs m') tst. +Proof. + intros. inv H2. pose proof H. inv H. inv H9. + destruct st. + econstructor; simplify. + { econstructor. + { econstructor; intros. rewrite genmap1; crush. } + { rewrite map2. econstructor; eauto. eapply gen_list_base. intros. rewrite <- H6. + eauto. specialize (H6 r). rewrite H6. eauto. } } + { econstructor; eauto. } +Qed. + +Lemma sem_update : + forall A ge sp st x st' st'' st''' f, + sem ge sp st f st' -> + match_states st' st''' -> + @step_instr A ge sp st''' x st'' -> + exists tst, sem ge sp st (update f x) tst /\ match_states st'' tst. +Proof. + intros. destruct x; inv H1. + { econstructor. split. + apply sem_update_RBnop. eassumption. + apply match_states_commut. auto. } + { eapply sem_update_Op; eauto. } + { eapply sem_update_load; eauto. } + { eapply sem_update_store; eauto. } +Qed. + +Lemma sem_update2_Op : + forall A ge sp st f r l o0 o m rs v, + @sem A ge sp st f (mk_instr_state rs m) -> + Op.eval_operation ge sp o0 rs ## l m = Some v -> + sem ge sp st (update f (RBop o o0 l r)) (mk_instr_state (Regmap.set r v rs) m). +Proof. + intros. destruct st. constructor. + inv H. inv H6. + { constructor; intros. simplify. + destruct (Pos.eq_dec r x); subst. + { rewrite map2. econstructor. eauto. + apply gen_list_base. eauto. + rewrite Regmap.gss. auto. } + { rewrite genmap1; crush. rewrite Regmap.gso; auto. } } + { simplify. rewrite genmap1; crush. inv H. eauto. } +Qed. + +Lemma sem_update2_load : + forall A ge sp st f r o m a l m0 rs v a0, + @sem A ge sp st f (mk_instr_state rs m0) -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.loadv m m0 a0 = Some v -> + sem ge sp st (update f (RBload o m a l r)) (mk_instr_state (Regmap.set r v rs) m0). +Proof. + intros. simplify. inv H. inv H7. constructor. + { constructor; intros. destruct (Pos.eq_dec r x); subst. + { rewrite map2. rewrite Regmap.gss. econstructor; eauto. + apply gen_list_base; eauto. } + { rewrite genmap1; crush. rewrite Regmap.gso; eauto. } + } + { simplify. rewrite genmap1; crush. } +Qed. + +Lemma sem_update2_store : + forall A ge sp a0 m a l r o f st m' rs m0, + @sem A ge sp st f (mk_instr_state rs m0) -> + Op.eval_addressing ge sp a rs ## l = Some a0 -> + Mem.storev m m0 a0 rs !! r = Some m' -> + sem ge sp st (update f (RBstore o m a l r)) (mk_instr_state rs m'). +Proof. + intros. simplify. inv H. inv H7. constructor; simplify. + { econstructor; intros. rewrite genmap1; crush. } + { rewrite map2. econstructor; eauto. apply gen_list_base; eauto. } +Qed. + +Lemma sem_update2 : + forall A ge sp st x st' st'' f, + sem ge sp st f st' -> + @step_instr A ge sp st' x st'' -> + sem ge sp st (update f x) st''. +Proof. + intros. + destruct x; inv H0; + eauto using sem_update_RBnop, sem_update2_Op, sem_update2_load, sem_update2_store. +Qed. + +Lemma rtlblock_trans_correct : + forall bb ge sp st st', + RTLBlock.step_instr_list ge sp st bb st' -> + forall tst, + match_states st tst -> + exists tst', sem ge sp tst (abstract_sequence empty bb) tst' + /\ match_states st' tst'. +Proof. + induction bb using rev_ind; simplify. + { econstructor. simplify. apply abstract_interp_empty. + inv H. auto. } + { apply rtlblock_trans_correct' in H. inv_simp. + rewrite abstract_seq. + exploit IHbb; try eassumption; []; inv_simp. + exploit sem_update. apply H1. apply match_states_commut; eassumption. + eauto. inv_simp. econstructor. split. apply H3. + auto. } +Qed. + +Lemma abstr_sem_val_mem : + forall A B ge tge st tst sp a, + ge_preserved ge tge -> + forall v m, + (@sem_mem A ge sp st a m /\ match_states st tst -> @sem_mem B tge sp tst a m) /\ + (@sem_value A ge sp st a v /\ match_states st tst -> @sem_value B tge sp tst a v). +Proof. + intros * H. + apply expression_ind2 with + + (P := fun (e1: expression) => + forall v m, + (@sem_mem A ge sp st e1 m /\ match_states st tst -> @sem_mem B tge sp tst e1 m) /\ + (@sem_value A ge sp st e1 v /\ match_states st tst -> @sem_value B tge sp tst e1 v)) + + (P0 := fun (e1: expression_list) => + forall lv, @sem_val_list A ge sp st e1 lv /\ match_states st tst -> @sem_val_list B tge sp tst e1 lv); + simplify; intros; simplify. + { inv H1. inv H2. constructor. } + { inv H2. inv H1. rewrite H0. constructor. } + { inv H3. } + { inv H3. inv H4. econstructor. apply H1; auto. simplify. eauto. constructor. auto. auto. + apply H0; simplify; eauto. constructor; eauto. + unfold ge_preserved in *. simplify. rewrite <- H2. auto. + } + { inv H3. } + { inv H3. inv H4. econstructor. apply H1; eauto; simplify; eauto. constructor; eauto. + apply H0; simplify; eauto. constructor; eauto. + inv H. rewrite <- H4. eauto. + auto. + } + { inv H4. inv H5. econstructor. apply H0; eauto. simplify; eauto. constructor; eauto. + apply H2; eauto. simplify; eauto. constructor; eauto. + apply H1; eauto. simplify; eauto. constructor; eauto. + inv H. rewrite <- H5. eauto. auto. + } + { inv H4. } + { inv H1. constructor. } + { inv H3. constructor; auto. apply H0; eauto. apply Mem.empty. } +Qed. + +Lemma abstr_sem_value : + forall a A B ge tge sp st tst v, + @sem_value A ge sp st a v -> + ge_preserved ge tge -> + match_states st tst -> + @sem_value B tge sp tst a v. +Proof. intros; eapply abstr_sem_val_mem; eauto; apply Mem.empty. Qed. + +Lemma abstr_sem_mem : + forall a A B ge tge sp st tst v, + @sem_mem A ge sp st a v -> + ge_preserved ge tge -> + match_states st tst -> + @sem_mem B tge sp tst a v. +Proof. intros; eapply abstr_sem_val_mem; eauto. Qed. + +Lemma abstr_sem_regset : + forall a a' A B ge tge sp st tst rs, + @sem_regset A ge sp st a rs -> + ge_preserved ge tge -> + (forall x, a # x = a' # x) -> + match_states st tst -> + exists rs', @sem_regset B tge sp tst a' rs' /\ (forall x, rs !! x = rs' !! x). +Proof. + inversion 1; intros. + inv H7. + econstructor. simplify. econstructor. intros. + eapply abstr_sem_value; eauto. rewrite <- H6. + eapply H0. constructor; eauto. + auto. +Qed. + +Lemma abstr_sem : + forall a a' A B ge tge sp st tst st', + @sem A ge sp st a st' -> + ge_preserved ge tge -> + (forall x, a # x = a' # x) -> + match_states st tst -> + exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'. +Proof. + inversion 1; subst; intros. + inversion H4; subst. + exploit abstr_sem_regset; eauto; inv_simp. + do 3 econstructor; eauto. + rewrite <- H3. + eapply abstr_sem_mem; eauto. +Qed. + +Lemma abstract_execution_correct': + forall A B ge tge sp st' a a' st tst, + @sem A ge sp st a st' -> + ge_preserved ge tge -> + check a a' = true -> + match_states st tst -> + exists tst', @sem B tge sp tst a' tst' /\ match_states st' tst'. +Proof. + intros; + pose proof (check_correct a a' H1); + eapply abstr_sem; eauto. +Qed. + +Lemma states_match : + forall st1 st2 st3 st4, + match_states st1 st2 -> + match_states st2 st3 -> + match_states st3 st4 -> + match_states st1 st4. +Proof. + intros * H1 H2 H3; destruct st1; destruct st2; destruct st3; destruct st4. + inv H1. inv H2. inv H3; constructor. + unfold regs_lessdef in *. intros. + repeat match goal with + | H: forall _, _, r : positive |- _ => specialize (H r) + end. + congruence. + auto. +Qed. + +Lemma step_instr_block_same : + forall ge sp st st', + step_instr_block ge sp st nil st' -> + st = st'. +Proof. inversion 1; auto. Qed. + +Lemma step_instr_seq_same : + forall ge sp st st', + step_instr_seq ge sp st nil st' -> + st = st'. +Proof. inversion 1; auto. Qed. + +Lemma match_states_list : + forall A (rs: Regmap.t A) rs', + (forall r, rs !! r = rs' !! r) -> + forall l, rs ## l = rs' ## l. +Proof. induction l; crush. Qed. + +Lemma PTree_matches : + forall A (v: A) res rs rs', + (forall r, rs !! r = rs' !! r) -> + forall x, (Regmap.set res v rs) !! x = (Regmap.set res v rs') !! x. +Proof. + intros; destruct (Pos.eq_dec x res); subst; + [ repeat rewrite Regmap.gss by auto + | repeat rewrite Regmap.gso by auto ]; auto. +Qed. + +Lemma step_instr_matches : + forall A a ge sp st st', + @step_instr A ge sp st a st' -> + forall tst, match_states st tst -> + exists tst', step_instr ge sp tst a tst' + /\ match_states st' tst'. +Proof. + induction 1; simplify; + match goal with H: match_states _ _ |- _ => inv H end; + repeat econstructor; try erewrite match_states_list; + try apply PTree_matches; eauto; + match goal with + H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto + end. +Qed. + +Lemma step_instr_list_matches : + forall a ge sp st st', + step_instr_list ge sp st a st' -> + forall tst, match_states st tst -> + exists tst', step_instr_list ge sp tst a tst' + /\ match_states st' tst'. +Proof. + induction a; intros; inv H; + try (exploit step_instr_matches; eauto; []; inv_simp; + exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto. +Qed. + +Lemma step_instr_seq_matches : + forall a ge sp st st', + step_instr_seq ge sp st a st' -> + forall tst, match_states st tst -> + exists tst', step_instr_seq ge sp tst a tst' + /\ match_states st' tst'. +Proof. + induction a; intros; inv H; + try (exploit step_instr_list_matches; eauto; []; inv_simp; + exploit IHa; eauto; []; inv_simp); repeat econstructor; eauto. +Qed. + +Lemma step_instr_block_matches : + forall bb ge sp st st', + step_instr_block ge sp st bb st' -> + forall tst, match_states st tst -> + exists tst', step_instr_block ge sp tst bb tst' + /\ match_states st' tst'. +Proof. + induction bb; intros; inv H; + try (exploit step_instr_seq_matches; eauto; []; inv_simp; + exploit IHbb; eauto; []; inv_simp); repeat econstructor; eauto. +Qed. + +Lemma sem_update' : + forall A ge sp st a x st', + sem ge sp st (update (abstract_sequence empty a) x) st' -> + exists st'', + @step_instr A ge sp st'' x st' /\ + sem ge sp st (abstract_sequence empty a) st''. +Proof. + Admitted. + +Lemma sem_separate : + forall A (ge: @RTLBlockInstr.genv A) b a sp st st', + sem ge sp st (abstract_sequence empty (a ++ b)) st' -> + exists st'', + sem ge sp st (abstract_sequence empty a) st'' + /\ sem ge sp st'' (abstract_sequence empty b) st'. +Proof. + induction b using rev_ind; simplify. + { econstructor. simplify. rewrite app_nil_r in H. eauto. apply abstract_interp_empty. } + { simplify. rewrite app_assoc in H. rewrite abstract_seq in H. + exploit sem_update'; eauto; inv_simp. + exploit IHb; eauto; inv_simp. + econstructor; split; eauto. + rewrite abstract_seq. + eapply sem_update2; eauto. + } +Qed. + +Lemma rtlpar_trans_correct : + forall bb ge sp sem_st' sem_st st, + sem ge sp sem_st (abstract_sequence empty (concat (concat bb))) sem_st' -> + match_states sem_st st -> + exists st', RTLPar.step_instr_block ge sp st bb st' + /\ match_states sem_st' st'. +Proof. + induction bb using rev_ind. + { repeat econstructor. eapply abstract_interp_empty3 in H. + inv H. inv H0. constructor; congruence. } + { simplify. inv H0. repeat rewrite concat_app in H. simplify. + rewrite app_nil_r in H. + exploit sem_separate; eauto; inv_simp. + repeat econstructor. admit. admit. + } +Admitted. + Lemma abstract_execution_correct: - forall bb bb' cfi ge tge sp rs m rs' m', + forall bb bb' cfi ge tge sp st st' tst, + RTLBlock.step_instr_list ge sp st bb st' -> ge_preserved ge tge -> schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> - RTLBlock.step_instr_list ge sp (InstrState rs m) bb (InstrState rs' m') -> - exists rs'', RTLPar.step_instr_block tge sp (InstrState rs m) bb' (InstrState rs'' m') - /\ regs_lessdef rs' rs''. -Proof. Abort. + match_states st tst -> + exists tst', RTLPar.step_instr_block tge sp tst bb' tst' + /\ match_states st' tst'. +Proof. + intros. + unfold schedule_oracle in *. simplify. + exploit rtlblock_trans_correct; try eassumption; []; inv_simp. + exploit abstract_execution_correct'; + try solve [eassumption | apply state_lessdef_match_sem; eassumption]. + apply match_states_commut. eauto. inv_simp. + exploit rtlpar_trans_correct; try eassumption; []; inv_simp. + exploit step_instr_block_matches; eauto. apply match_states_commut; eauto. inv_simp. + repeat match goal with | H: match_states _ _ |- _ => inv H end. + do 2 econstructor; eauto. + econstructor; congruence. +Qed. + +(*Lemma abstract_execution_correct_ld: + forall bb bb' cfi ge tge sp st st' tst, + RTLBlock.step_instr_list ge sp st bb st' -> + ge_preserved ge tge -> + schedule_oracle (mk_bblock bb cfi) (mk_bblock bb' cfi) = true -> + match_states_ld st tst -> + exists tst', RTLPar.step_instr_block tge sp tst bb' tst' + /\ match_states st' tst'. +Proof. + intros.*) +*) (*| Top-level functions @@ -677,16 +1120,7 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function : else Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent."). -Definition transl_function_temp (f: RTLBlock.function) : Errors.res RTLPar.function := - let tfcode := fn_code (schedule f) in - Errors.OK (mkfunction f.(fn_sig) - f.(fn_params) - f.(fn_stacksize) - tfcode - f.(fn_entrypoint)). - -Definition transl_fundef := transf_partial_fundef transl_function_temp. +Definition transl_fundef := transf_partial_fundef transl_function. Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program := transform_partial_program transl_fundef p. -*) diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v index a0c01fa..bb1cf97 100644 --- a/src/hls/RTLPargenproof.v +++ b/src/hls/RTLPargenproof.v @@ -38,34 +38,29 @@ Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop := | match_stackframe: forall f tf res sp pc rs rs', transl_function f = OK tf -> - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> match_stackframes (Stackframe res f sp pc rs) (Stackframe res tf sp pc rs'). Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop := | match_state: - forall sf f sp pc rs rs' m m' sf' tf + forall sf f sp pc rs rs' m sf' tf (TRANSL: transl_function f = OK tf) (STACKS: list_forall2 match_stackframes sf sf') - (REG: regs_lessdef rs rs') - (MEM: Mem.extends m m'), + (REG: forall x, rs !! x = rs' !! x), match_states (State sf f sp pc rs m) - (State sf' tf sp pc rs' m') + (State sf' tf sp pc rs' m) | match_returnstate: - forall stack stack' v v' m m' - (STACKS: list_forall2 match_stackframes stack stack') - (MEM: Mem.extends m m') - (LD: Val.lessdef v v'), + forall stack stack' v m + (STACKS: list_forall2 match_stackframes stack stack'), match_states (Returnstate stack v m) - (Returnstate stack' v' m') + (Returnstate stack' v m) | match_callstate: - forall stack stack' f tf args args' m m' + forall stack stack' f tf args m (TRANSL: transl_fundef f = OK tf) - (STACKS: list_forall2 match_stackframes stack stack') - (LD: Val.lessdef_list args args') - (MEM: Mem.extends m m'), + (STACKS: list_forall2 match_stackframes stack stack'), match_states (Callstate stack f args m) - (Callstate stack' tf args' m'). + (Callstate stack' tf args m). Section CORRECTNESS. @@ -121,7 +116,7 @@ Section CORRECTNESS. Lemma find_function_translated: forall ros rs rs' f, - regs_lessdef rs rs' -> + (forall x, rs !! x = rs' !! x) -> find_function ge ros rs = Some f -> exists tf, find_function tge ros rs' = Some tf /\ transl_fundef f = OK tf. @@ -134,7 +129,7 @@ Section CORRECTNESS. | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H] | _ => solve [exploit functions_translated; eauto] end. - unfold regs_lessdef; destruct ros; simplify; try rewrite <- H; + destruct ros; simplify; try rewrite <- H; [| rewrite symbols_preserved; destruct_match; try (apply function_ptr_translated); crush ]; intros; @@ -160,8 +155,8 @@ Section CORRECTNESS. Qed. Lemma eval_op_eq: - forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val), - Op.eval_operation ge sp0 op vl = Op.eval_operation tge sp0 op vl. + forall (sp0 : Values.val) (op : Op.operation) (vl : list Values.val) m, + Op.eval_operation ge sp0 op vl m = Op.eval_operation tge sp0 op vl m. Proof using TRANSL. intros. destruct op; auto; unfold Op.eval_operation, Genv.symbol_address, Op.eval_addressing32; @@ -197,6 +192,16 @@ Section CORRECTNESS. Proof using. destruct or; crush. Qed. Hint Resolve lessdef_regmap_optget : rtlgp. + Lemma regmap_equiv_lessdef: + forall rs rs', + (forall x, rs !! x = rs' !! x) -> + regs_lessdef rs rs'. + Proof using. + intros; unfold regs_lessdef; intros. + rewrite H. apply Val.lessdef_refl. + Qed. + Hint Resolve regmap_equiv_lessdef : rtlgp. + Lemma int_lessdef: forall rs rs', regs_lessdef rs rs' -> @@ -227,8 +232,8 @@ Section CORRECTNESS. let H2 := fresh "SCHED" in learn H as H2; apply schedule_oracle_nil in H2 - | [ H: find_function _ _ _ = Some _ |- _ ] => - learn H; exploit find_function_translated; eauto; inversion 1 + | [ H: find_function _ _ _ = Some _, H2: forall x, ?rs !! x = ?rs' !! x |- _ ] => + learn H; exploit find_function_translated; try apply H2; eauto; inversion 1 | [ H: Mem.free ?m _ _ _ = Some ?m', H2: Mem.extends ?m ?m'' |- _ ] => learn H; exploit Mem.free_parallel_extends; eauto; intros | [ H: Events.eval_builtin_args _ _ _ _ _ _, H2: regs_lessdef ?rs ?rs' |- _ ] => @@ -249,6 +254,29 @@ Section CORRECTNESS. Hint Resolve set_reg_lessdef : rtlgp. Hint Resolve Op.eval_condition_lessdef : rtlgp. + Hint Constructors Events.eval_builtin_arg: barg. + + Lemma eval_builtin_arg_eq: + forall A ge a v1 m1 e1 e2 sp, + (forall x, e1 x = e2 x) -> + @Events.eval_builtin_arg A ge e1 sp m1 a v1 -> + Events.eval_builtin_arg ge e2 sp m1 a v1. +Proof. induction 2; try rewrite H; eauto with barg. Qed. + + Lemma eval_builtin_args_eq: + forall A ge e1 sp m1 e2 al vl1, + (forall x, e1 x = e2 x) -> + @Events.eval_builtin_args A ge e1 sp m1 al vl1 -> + Events.eval_builtin_args ge e2 sp m1 al vl1. + Proof. + induction 2. + - econstructor; split. + - exploit eval_builtin_arg_eq; eauto. intros. + destruct IHlist_forall2 as [| y]. constructor; eauto. + constructor. constructor; auto. + constructor; eauto. + Qed. + Lemma step_cf_instr_correct: forall cfi t s s', step_cf_instr ge s cfi t s' -> @@ -257,7 +285,22 @@ Section CORRECTNESS. exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'. Proof using TRANSL. induction 1; repeat semantics_simpl; - repeat (econstructor; eauto with rtlgp). + try solve [repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp)]. + { do 3 (try erewrite match_states_list by eauto; econstructor; eauto with rtlgp). + eapply eval_builtin_args_eq. eapply REG. + eapply Events.eval_builtin_args_preserved. eapply symbols_preserved. + eauto. + intros. + unfold regmap_setres. destruct res. + destruct (Pos.eq_dec x0 x); subst. + repeat rewrite Regmap.gss; auto. + repeat rewrite Regmap.gso; auto. + eapply REG. eapply REG. + } + { repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp). + unfold regmap_optget. destruct or. rewrite REG. constructor; eauto. + constructor; eauto. + } Qed. Theorem transl_step_correct : @@ -269,21 +312,69 @@ Section CORRECTNESS. Proof. induction 1; repeat semantics_simpl. - Abort. - -(* { destruct bb as [bbc bbe]; destruct x as [bbc' bbe']. - assert (bbe = bbe') by admit. - rewrite H3 in H5. - eapply abstract_execution_correct in H5; eauto with rtlgp. - repeat econstructor; eauto with rtlgp. simplify. - exploit step_cf_instr_correct. eauto. - econstructor; eauto with rtlgp. + + { destruct bb; destruct x. + assert (bb_exit = bb_exit0). + { unfold schedule_oracle in *. simplify. + unfold check_control_flow_instr in *. + destruct_match; crush. + } + subst. + + exploit abstract_execution_correct; try eassumption. eapply ge_preserved_lem. + econstructor; eauto. + inv_simp. destruct x. inv H7. + + exploit step_cf_instr_correct; try eassumption. econstructor; eauto. + inv_simp. + + econstructor. econstructor. eapply Smallstep.plus_one. econstructor. + eauto. eauto. simplify. eauto. eauto. + } + { unfold bind in *. inv TRANSL0. clear Learn. inv H0. destruct_match; crush. + inv H2. unfold transl_function in Heqr. destruct_match; crush. + inv Heqr. + repeat econstructor; eauto. + unfold bind in *. destruct_match; crush. } - { unfold bind in *. destruct_match; try discriminate. repeat semantics_simpl. inv TRANSL0. - repeat econstructor; eauto. } { inv TRANSL0. repeat econstructor; eauto using Events.external_call_symbols_preserved, symbols_preserved, senv_preserved, Events.E0_right. } - { inv STACKS. inv H2. repeat econstructor; eauto. } - Qed.*) + { inv STACKS. inv H2. repeat econstructor; eauto. + intros. apply PTree_matches; eauto. + } + Qed. + + Lemma transl_initial_states: + forall S, + RTLBlock.initial_state prog S -> + exists R, RTLPar.initial_state tprog R /\ match_states S R. + Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + econstructor; split. + econstructor. apply (Genv.init_mem_transf_partial TRANSL); eauto. + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto. + symmetry; eapply match_program_main; eauto. + eexact A. + rewrite <- H2. apply sig_transl_function; auto. + constructor. auto. constructor. + Qed. + + Lemma transl_final_states: + forall S R r, + match_states S R -> RTLBlock.final_state S r -> RTLPar.final_state R r. + Proof. + intros. inv H0. inv H. inv STACKS. constructor. + Qed. + + Theorem transf_program_correct: + Smallstep.forward_simulation (RTLBlock.semantics prog) (RTLPar.semantics tprog). + Proof. + eapply Smallstep.forward_simulation_plus. + apply senv_preserved. + eexact transl_initial_states. + eexact transl_final_states. + exact transl_step_correct. + Qed. End CORRECTNESS. *) diff --git a/src/hls/Sat.v b/src/hls/Sat.v index 9549947..098eef1 100644 --- a/src/hls/Sat.v +++ b/src/hls/Sat.v @@ -146,7 +146,7 @@ Lemma contradictory_assignment : forall s l cl a, tauto. Qed. -Local Hint Resolve contradictory_assignment : core. +#[local] Hint Resolve contradictory_assignment : core. (** Augment an assignment with a new mapping. *) Definition upd (a : asgn) (l : lit) : asgn := @@ -163,7 +163,7 @@ Lemma satLit_upd_eq : forall l a, destruct (eq_nat_dec (snd l) (snd l)); tauto. Qed. -Local Hint Resolve satLit_upd_eq : core. +#[local] Hint Resolve satLit_upd_eq : core. Lemma satLit_upd_neq : forall v l s a, v <> snd l @@ -173,7 +173,7 @@ Lemma satLit_upd_neq : forall v l s a, destruct (eq_nat_dec v (snd l)); tauto. Qed. -Local Hint Resolve satLit_upd_neq : core. +#[local] Hint Resolve satLit_upd_neq : core. Lemma satLit_upd_neq2 : forall v l s a, v <> snd l @@ -183,7 +183,7 @@ Lemma satLit_upd_neq2 : forall v l s a, destruct (eq_nat_dec v (snd l)); tauto. Qed. -Local Hint Resolve satLit_upd_neq2 : core. +#[local] Hint Resolve satLit_upd_neq2 : core. Lemma satLit_contra : forall s l a cl, s <> fst l @@ -194,7 +194,7 @@ Lemma satLit_contra : forall s l a cl, assert False; intuition. Qed. -Local Hint Resolve satLit_contra : core. +#[local] Hint Resolve satLit_contra : core. (** Here's the tactic that I used to discharge #<i>#all#</i># proof obligations in my implementations of the four functions you will define. @@ -202,9 +202,9 @@ Local Hint Resolve satLit_contra : core. obligations that it can't solve, or obligations that it takes 42 years to solve. However, if you think enough like me, each of the four definitions you fill in - should read like: [[ + should read like: refine some_expression_with_holes; clear function_name; magic_solver. -]] leaving out the [clear] invocation for non-recursive function definitions. + leaving out the [clear] invocation for non-recursive function definitions. *) Ltac magic_solver := simpl; intros; subst; intuition eauto; firstorder; match goal with @@ -288,7 +288,7 @@ Lemma satLit_idem_lit : forall l a l', destruct (eq_nat_dec (snd l') (snd l)); congruence. Qed. -Local Hint Resolve satLit_idem_lit : core. +#[local] Hint Resolve satLit_idem_lit : core. Lemma satLit_idem_clause : forall l a cl, satLit l a @@ -297,7 +297,7 @@ Lemma satLit_idem_clause : forall l a cl, induction cl; simpl; intuition. Qed. -Local Hint Resolve satLit_idem_clause : core. +#[local] Hint Resolve satLit_idem_clause : core. Lemma satLit_idem_formula : forall l a fm, satLit l a @@ -306,7 +306,7 @@ Lemma satLit_idem_formula : forall l a fm, induction fm; simpl; intuition. Qed. -Local Hint Resolve satLit_idem_formula : core. +#[local] Hint Resolve satLit_idem_formula : core. (** Challenge 2: Write this function that updates an entire formula to reflect setting a literal to true. @@ -349,7 +349,7 @@ Eval compute in setFormulaSimple (((false, 1) :: nil) :: nil) (true, 0). Eval compute in setFormulaSimple (((false, 1) :: (true, 0) :: nil) :: nil) (true, 0). Eval compute in setFormulaSimple (((false, 1) :: (false, 0) :: nil) :: nil) (true, 0).*) -Local Hint Extern 1 False => discriminate : core. +#[local] Hint Extern 1 False => discriminate : core. Local Hint Extern 1 False => match goal with @@ -366,7 +366,7 @@ Definition findUnitClause : forall (fm: formula), match fm with | nil => inright _ | (l :: nil) :: fm' => inleft (exist _ l _) - | cl :: fm' => + | _ :: fm' => match findUnitClause fm' with | inleft (exist _ l _) => inleft (exist _ l _) | inright H => inright _ @@ -387,7 +387,7 @@ Lemma unitClauseTrue : forall l a fm, inversion H; subst; simpl in H0; intuition. Qed. -Local Hint Resolve unitClauseTrue : core. +#[local] Hint Resolve unitClauseTrue : core. (** Final challenge: Implement unit propagation. The return type of [unitPropagate] signifies that three results are possible: @@ -447,7 +447,7 @@ Definition chooseSplit (fm : formula) := Definition negate (l : lit) := (negb (fst l), snd l). -Local Hint Unfold satFormula : core. +#[local] Hint Unfold satFormula : core. Lemma satLit_dec : forall l a, {satLit l a} + {satLit (negate l) a}. diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml new file mode 100644 index 0000000..2389369 --- /dev/null +++ b/src/hls/Schedule.ml @@ -0,0 +1,831 @@ +(* + * Vericert: Verified high-level synthesis. + * Copyright (C) 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/>. + *) + +open Printf +open Clflags +open Camlcoq +open Datatypes +open Coqlib +open Maps +open AST +open Kildall +open Op +open RTLBlockInstr +open RTLBlock +open HTL +open Verilog +open HTLgen +open HTLMonad +open HTLMonadExtra + +module SS = Set.Make(P) + +type svtype = + | BBType of int + | VarType of int * int + +type sv = { + sv_type: svtype; + sv_num: int; +} + +let print_sv v = + match v with + | { sv_type = BBType bbi; sv_num = n } -> sprintf "bb%d_%d" bbi n + | { sv_type = VarType (bbi, i); sv_num = n } -> sprintf "var%dn%d_%d" bbi i n + +module G = Graph.Persistent.Digraph.ConcreteLabeled(struct + type t = sv + let compare = compare + let equal = (=) + let hash = Hashtbl.hash +end)(struct + type t = int + let compare = compare + let hash = Hashtbl.hash + let equal = (=) + let default = 0 +end) + +module GDot = Graph.Graphviz.Dot(struct + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_name = print_sv + let vertex_attributes _ = [] + let get_subgraph _ = None + let default_edge_attributes _ = [] + let edge_attributes _ = [] + + include G + end) + +module DFG = Graph.Persistent.Digraph.ConcreteLabeled(struct + type t = int * instr + let compare = compare + let equal = (=) + let hash = Hashtbl.hash +end)(struct + type t = int + let compare = compare + let hash = Hashtbl.hash + let equal = (=) + let default = 0 +end) + +module DFGSimp = Graph.Persistent.Graph.Concrete(struct + type t = int * instr + let compare = compare + let equal = (=) + let hash = Hashtbl.hash + end) + +let convert dfg = + DFG.fold_vertex (fun v g -> DFGSimp.add_vertex g v) dfg DFGSimp.empty + |> DFG.fold_edges (fun v1 v2 g -> DFGSimp.add_edge (DFGSimp.add_edge g v1 v2) v2 v1) dfg + +let reg r = sprintf "r%d" (P.to_int r) +let print_pred r = sprintf "p%d" (P.to_int r) + +let print_instr = function + | RBnop -> "" + | RBload (_, _, _, _, r) -> sprintf "load(%s)" (reg r) + | RBstore (_, _, _, _, r) -> sprintf "store(%s)" (reg r) + | RBsetpred (_, _, p) -> sprintf "setpred(%s)" (print_pred p) + | RBop (_, op, args, d) -> + (match op, args with + | Omove, _ -> "mov" + | Ointconst n, _ -> sprintf "%s=%ld" (reg d) (camlint_of_coqint n) + | Olongconst n, _ -> sprintf "%s=%LdL" (reg d) (camlint64_of_coqint n) + | Ofloatconst n, _ -> sprintf "%s=%.15F" (reg d) (camlfloat_of_coqfloat n) + | Osingleconst n, _ -> sprintf "%s=%.15Ff" (reg d) (camlfloat_of_coqfloat32 n) + | Oindirectsymbol id, _ -> sprintf "%s=&%s" (reg d) (extern_atom id) + | Ocast8signed, [r1] -> sprintf "%s=int8signed(%s)" (reg d) (reg r1) + | Ocast8unsigned, [r1] -> sprintf "%s=int8unsigned(%s)" (reg d) (reg r1) + | Ocast16signed, [r1] -> sprintf "%s=int16signed(%s)" (reg d) (reg r1) + | Ocast16unsigned, [r1] -> sprintf "%s=int16unsigned(%s)" (reg d) (reg r1) + | Oneg, [r1] -> sprintf "%s=-%s" (reg d) (reg r1) + | Osub, [r1;r2] -> sprintf "%s=%s-%s" (reg d) (reg r1) (reg r2) + | Omul, [r1;r2] -> sprintf "%s=%s*%s" (reg d) (reg r1) (reg r2) + | Omulimm n, [r1] -> sprintf "%s=%s*%ld" (reg d) (reg r1) (camlint_of_coqint n) + | Omulhs, [r1;r2] -> sprintf "%s=mulhs(%s,%s)" (reg d) (reg r1) (reg r2) + | Omulhu, [r1;r2] -> sprintf "%s=mulhu(%s,%s)" (reg d) (reg r1) (reg r2) + | Odiv, [r1;r2] -> sprintf "%s=%s /s %s" (reg d) (reg r1) (reg r2) + | Odivu, [r1;r2] -> sprintf "%s=%s /u %s" (reg d) (reg r1) (reg r2) + | Omod, [r1;r2] -> sprintf "%s=%s %%s %s" (reg d) (reg r1) (reg r2) + | Omodu, [r1;r2] -> sprintf "%s=%s %%u %s" (reg d) (reg r1) (reg r2) + | Oand, [r1;r2] -> sprintf "%s=%s & %s" (reg d) (reg r1) (reg r2) + | Oandimm n, [r1] -> sprintf "%s=%s & %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oor, [r1;r2] -> sprintf "%s=%s | %s" (reg d) (reg r1) (reg r2) + | Oorimm n, [r1] -> sprintf "%s=%s | %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oxor, [r1;r2] -> sprintf "%s=%s ^ %s" (reg d) (reg r1) (reg r2) + | Oxorimm n, [r1] -> sprintf "%s=%s ^ %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Onot, [r1] -> sprintf "%s=not(%s)" (reg d) (reg r1) + | Oshl, [r1;r2] -> sprintf "%s=%s << %s" (reg d) (reg r1) (reg r2) + | Oshlimm n, [r1] -> sprintf "%s=%s << %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshr, [r1;r2] -> sprintf "%s=%s >>s %s" (reg d) (reg r1) (reg r2) + | Oshrimm n, [r1] -> sprintf "%s=%s >>s %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrximm n, [r1] -> sprintf "%s=%s >>x %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshru, [r1;r2] -> sprintf "%s=%s >>u %s" (reg d) (reg r1) (reg r2) + | Oshruimm n, [r1] -> sprintf "%s=%s >>u %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Ororimm n, [r1] -> sprintf "%s=%s ror %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshldimm n, [r1;r2] -> sprintf "%s=(%s, %s) << %ld" (reg d) (reg r1) (reg r2) (camlint_of_coqint n) + | Olea addr, args -> sprintf "%s=addr" (reg d) + | Omakelong, [r1;r2] -> sprintf "%s=makelong(%s,%s)" (reg d) (reg r1) (reg r2) + | Olowlong, [r1] -> sprintf "%s=lowlong(%s)" (reg d) (reg r1) + | Ohighlong, [r1] -> sprintf "%s=highlong(%s)" (reg d) (reg r1) + | Ocast32signed, [r1] -> sprintf "%s=long32signed(%s)" (reg d) (reg r1) + | Ocast32unsigned, [r1] -> sprintf "%s=long32unsigned(%s)" (reg d) (reg r1) + | Onegl, [r1] -> sprintf "%s=-l %s" (reg d) (reg r1) + | Osubl, [r1;r2] -> sprintf "%s=%s -l %s" (reg d) (reg r1) (reg r2) + | Omull, [r1;r2] -> sprintf "%s=%s *l %s" (reg d) (reg r1) (reg r2) + | Omullimm n, [r1] -> sprintf "%s=%s *l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Omullhs, [r1;r2] -> sprintf "%s=mullhs(%s,%s)" (reg d) (reg r1) (reg r2) + | Omullhu, [r1;r2] -> sprintf "%s=mullhu(%s,%s)" (reg d) (reg r1) (reg r2) + | Odivl, [r1;r2] -> sprintf "%s=%s /ls %s" (reg d) (reg r1) (reg r2) + | Odivlu, [r1;r2] -> sprintf "%s=%s /lu %s" (reg d) (reg r1) (reg r2) + | Omodl, [r1;r2] -> sprintf "%s=%s %%ls %s" (reg d) (reg r1) (reg r2) + | Omodlu, [r1;r2] -> sprintf "%s=%s %%lu %s" (reg d) (reg r1) (reg r2) + | Oandl, [r1;r2] -> sprintf "%s=%s &l %s" (reg d) (reg r1) (reg r2) + | Oandlimm n, [r1] -> sprintf "%s=%s &l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Oorl, [r1;r2] -> sprintf "%s=%s |l %s" (reg d) (reg r1) (reg r2) + | Oorlimm n, [r1] -> sprintf "%s=%s |l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Oxorl, [r1;r2] -> sprintf "%s=%s ^l %s" (reg d) (reg r1) (reg r2) + | Oxorlimm n, [r1] -> sprintf "%s=%s ^l %Ld" (reg d) (reg r1) (camlint64_of_coqint n) + | Onotl, [r1] -> sprintf "%s=notl(%s)" (reg d) (reg r1) + | Oshll, [r1;r2] -> sprintf "%s=%s <<l %s" (reg d) (reg r1) (reg r2) + | Oshllimm n, [r1] -> sprintf "%s=%s <<l %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrl, [r1;r2] -> sprintf "%s=%s >>ls %s" (reg d) (reg r1) (reg r2) + | Oshrlimm n, [r1] -> sprintf "%s=%s >>ls %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrxlimm n, [r1] -> sprintf "%s=%s >>lx %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oshrlu, [r1;r2] -> sprintf "%s=%s >>lu %s" (reg d) (reg r1) (reg r2) + | Oshrluimm n, [r1] -> sprintf "%s=%s >>lu %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Ororlimm n, [r1] -> sprintf "%s=%s rorl %ld" (reg d) (reg r1) (camlint_of_coqint n) + | Oleal addr, args -> sprintf "%s=addr" (reg d) + | Onegf, [r1] -> sprintf "%s=negf(%s)" (reg d) (reg r1) + | Oabsf, [r1] -> sprintf "%s=absf(%s)" (reg d) (reg r1) + | Oaddf, [r1;r2] -> sprintf "%s=%s +f %s" (reg d) (reg r1) (reg r2) + | Osubf, [r1;r2] -> sprintf "%s=%s -f %s" (reg d) (reg r1) (reg r2) + | Omulf, [r1;r2] -> sprintf "%s=%s *f %s" (reg d) (reg r1) (reg r2) + | Odivf, [r1;r2] -> sprintf "%s=%s /f %s" (reg d) (reg r1) (reg r2) + | Onegfs, [r1] -> sprintf "%s=negfs(%s)" (reg d) (reg r1) + | Oabsfs, [r1] -> sprintf "%s=absfs(%s)" (reg d) (reg r1) + | Oaddfs, [r1;r2] -> sprintf "%s=%s +fs %s" (reg d) (reg r1) (reg r2) + | Osubfs, [r1;r2] -> sprintf "%s=%s -fs %s" (reg d) (reg r1) (reg r2) + | Omulfs, [r1;r2] -> sprintf "%s=%s *fs %s" (reg d) (reg r1) (reg r2) + | Odivfs, [r1;r2] -> sprintf "%s=%s /fs %s" (reg d) (reg r1) (reg r2) + | Osingleoffloat, [r1] -> sprintf "%s=singleoffloat(%s)" (reg d) (reg r1) + | Ofloatofsingle, [r1] -> sprintf "%s=floatofsingle(%s)" (reg d) (reg r1) + | Ointoffloat, [r1] -> sprintf "%s=intoffloat(%s)" (reg d) (reg r1) + | Ofloatofint, [r1] -> sprintf "%s=floatofint(%s)" (reg d) (reg r1) + | Ointofsingle, [r1] -> sprintf "%s=intofsingle(%s)" (reg d) (reg r1) + | Osingleofint, [r1] -> sprintf "%s=singleofint(%s)" (reg d) (reg r1) + | Olongoffloat, [r1] -> sprintf "%s=longoffloat(%s)" (reg d) (reg r1) + | Ofloatoflong, [r1] -> sprintf "%s=floatoflong(%s)" (reg d) (reg r1) + | Olongofsingle, [r1] -> sprintf "%s=longofsingle(%s)" (reg d) (reg r1) + | Osingleoflong, [r1] -> sprintf "%s=singleoflong(%s)" (reg d) (reg r1) + | Ocmp c, args -> sprintf "%s=cmp" (reg d) + | Osel (c, ty), r1::r2::args -> sprintf "%s=sel" (reg d) + | _, _ -> sprintf "N/a") + +module DFGDot = Graph.Graphviz.Dot(struct + let graph_attributes _ = [] + let default_vertex_attributes _ = [] + let vertex_name = function (i, instr) -> sprintf "\"%d:%s\"" i (print_instr instr) + let vertex_attributes _ = [] + let get_subgraph _ = None + let default_edge_attributes _ = [] + let edge_attributes _ = [] + + include DFG + end) + +module DFGDfs = Graph.Traverse.Dfs(DFG) + +module IMap = Map.Make (struct + type t = int + + let compare = compare +end) + +let gen_vertex instrs i = (i, List.nth instrs i) + +(** The DFG type defines a list of instructions with their data dependencies as [edges], which are + the pairs of integers that represent the index of the instruction in the [nodes]. The edges + always point from left to right. *) + +let print_list f out_chan a = + fprintf out_chan "[ "; + List.iter (fprintf out_chan "%a " f) a; + fprintf out_chan "]" + +let print_tuple out_chan a = + let l, r = a in + fprintf out_chan "(%d,%d)" l r + +(*let print_dfg out_chan dfg = + fprintf out_chan "{ nodes = %a, edges = %a }" + (print_list PrintRTLBlockInstr.print_bblock_body) + dfg.nodes (print_list print_tuple) dfg.edges*) + +let print_dfg = DFGDot.output_graph + +let read_process command = + let buffer_size = 2048 in + let buffer = Buffer.create buffer_size in + let string = Bytes.create buffer_size in + let in_channel = Unix.open_process_in command in + let chars_read = ref 1 in + while !chars_read <> 0 do + chars_read := input in_channel string 0 buffer_size; + Buffer.add_substring buffer (Bytes.to_string string) 0 !chars_read + done; + ignore (Unix.close_process_in in_channel); + Buffer.contents buffer + +let comb_delay = function + | RBnop -> 0 + | RBop (_, op, _, _) -> + (match op with + | Omove -> 0 + | Ointconst _ -> 0 + | Olongconst _ -> 0 + | Ocast8signed -> 0 + | Ocast8unsigned -> 0 + | Ocast16signed -> 0 + | Ocast16unsigned -> 0 + | Oneg -> 0 + | Onot -> 0 + | Oor -> 0 + | Oorimm _ -> 0 + | Oand -> 0 + | Oandimm _ -> 0 + | Oxor -> 0 + | Oxorimm _ -> 0 + | Omul -> 8 + | Omulimm _ -> 8 + | Omulhs -> 8 + | Omulhu -> 8 + | Odiv -> 72 + | Odivu -> 72 + | Omod -> 72 + | Omodu -> 72 + | _ -> 1) + | _ -> 1 + +let pipeline_stages = function + | RBop (_, op, _, _) -> + (match op with + | Odiv -> 32 + | Odivu -> 32 + | Omod -> 32 + | Omodu -> 32 + | _ -> 0) + | _ -> 0 + +(** Add a dependency if it uses a register that was written to previously. *) +let add_dep map i tree dfg curr = + match PTree.get curr tree with + | None -> dfg + | Some ip -> + let ipv = (List.nth map ip) in + DFG.add_edge_e dfg (ipv, comb_delay (snd ipv), List.nth map i) + +(** This function calculates the dependencies of each instruction. The nodes correspond to previous + registers that were allocated and show which instruction caused it. + + This function only gathers the RAW constraints, and will therefore only be active for operations + that modify registers, which is this case only affects loads and operations. *) +let accumulate_RAW_deps map dfg curr = + let i, dst_map, graph = dfg in + let acc_dep_instruction rs dst = + ( i + 1, + PTree.set dst i dst_map, + List.fold_left (add_dep map i dst_map) graph rs + ) + in + let acc_dep_instruction_nodst rs = + ( i + 1, + dst_map, + List.fold_left (add_dep map i dst_map) graph rs) + in + match curr with + | RBop (op, _, rs, dst) -> acc_dep_instruction rs dst + | RBload (op, _mem, _addr, rs, dst) -> acc_dep_instruction rs dst + | RBstore (op, _mem, _addr, rs, src) -> acc_dep_instruction_nodst (src :: rs) + | _ -> (i + 1, dst_map, graph) + +(** Finds the next write to the [dst] register. This is a small optimisation so that only one + dependency is generated for a data dependency. *) +let rec find_next_dst_write i dst i' curr = + let check_dst dst' curr' = + if dst = dst' then Some (i, i') + else find_next_dst_write i dst (i' + 1) curr' + in + match curr with + | [] -> None + | RBop (_, _, _, dst') :: curr' -> check_dst dst' curr' + | RBload (_, _, _, _, dst') :: curr' -> check_dst dst' curr' + | _ :: curr' -> find_next_dst_write i dst (i' + 1) curr' + +let rec find_all_next_dst_read i dst i' curr = + let check_dst rs curr' = + if List.exists (fun x -> x = dst) rs + then (i, i') :: find_all_next_dst_read i dst (i' + 1) curr' + else find_all_next_dst_read i dst (i' + 1) curr' + in + match curr with + | [] -> [] + | RBop (_, _, rs, _) :: curr' -> check_dst rs curr' + | RBload (_, _, _, rs, _) :: curr' -> check_dst rs curr' + | RBstore (_, _, _, rs, src) :: curr' -> check_dst (src :: rs) curr' + | RBnop :: curr' -> find_all_next_dst_read i dst (i' + 1) curr' + | RBsetpred (_, rs, _) :: curr' -> check_dst rs curr' + +let drop i lst = + let rec drop' i' lst' = + match lst' with + | _ :: ls -> if i' = i then ls else drop' (i' + 1) ls + | [] -> [] + in + if i = 0 then lst else drop' 1 lst + +let take i lst = + let rec take' i' lst' = + match lst' with + | l :: ls -> if i' = i then [ l ] else l :: take' (i' + 1) ls + | [] -> [] + in + if i = 0 then [] else take' 1 lst + +let rec next_store i = function + | [] -> None + | RBstore (_, _, _, _, _) :: _ -> Some i + | _ :: rst -> next_store (i + 1) rst + +let rec next_load i = function + | [] -> None + | RBload (_, _, _, _, _) :: _ -> Some i + | _ :: rst -> next_load (i + 1) rst + +let accumulate_RAW_mem_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBload (_, _, _, _, _) -> ( + match next_store 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAR_mem_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBstore (_, _, _, _, _) -> ( + match next_load 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAW_mem_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBstore (_, _, _, _, _) -> ( + match next_store 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +(** Predicate dependencies. *) + +let rec in_predicate p p' = + match p' with + | Pvar p'' -> P.to_int p = P.to_int p'' + | Pnot p'' -> in_predicate p p'' + | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2 + | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2 + +let get_predicate = function + | RBop (p, _, _, _) -> p + | RBload (p, _, _, _, _) -> p + | RBstore (p, _, _, _, _) -> p + | _ -> None + +let rec next_setpred p i = function + | [] -> None + | RBsetpred (_, _, p') :: rst -> + if in_predicate p' p then + Some i + else + next_setpred p (i + 1) rst + | _ :: rst -> next_setpred p (i + 1) rst + +let rec next_preduse p i instr= + let next p' rst = + if in_predicate p p' then + Some i + else + next_preduse p (i + 1) rst + in + match instr with + | [] -> None + | RBload (Some p', _, _, _, _) :: rst -> next p' rst + | RBstore (Some p', _, _, _, _) :: rst -> next p' rst + | RBop (Some p', _, _, _) :: rst -> next p' rst + | _ :: rst -> next_load (i + 1) rst + +let accumulate_RAW_pred_deps instrs dfg curri = + let i, curr = curri in + match get_predicate curr with + | Some p -> ( + match next_setpred p 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAR_pred_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBsetpred (_, _, p) -> ( + match next_preduse p 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +let accumulate_WAW_pred_deps instrs dfg curri = + let i, curr = curri in + match curr with + | RBsetpred (_, _, p) -> ( + match next_setpred (Pvar p) 0 (take i instrs |> List.rev) with + | None -> dfg + | Some d -> DFG.add_edge dfg (gen_vertex instrs (i - d - 1)) (gen_vertex instrs i) ) + | _ -> dfg + +(** This function calculates the WAW dependencies, which happen when two writes are ordered one + after another and therefore have to be kept in that order. This accumulation might be redundant + if register renaming is done before hand, because then these dependencies can be avoided. *) +let accumulate_WAW_deps instrs dfg curri = + let i, curr = curri in + let dst_dep dst = + match find_next_dst_write i dst (i + 1) (drop (i + 1) instrs) with + | Some (a, b) -> DFG.add_edge dfg (gen_vertex instrs a) (gen_vertex instrs b) + | _ -> dfg + in + match curr with + | RBop (_, _, _, dst) -> dst_dep dst + | RBload (_, _, _, _, dst) -> dst_dep dst + | RBstore (_, _, _, _, _) -> ( + match next_store (i + 1) (drop (i + 1) instrs) with + | None -> dfg + | Some i' -> DFG.add_edge dfg (gen_vertex instrs i) (gen_vertex instrs i') ) + | _ -> dfg + +let accumulate_WAR_deps instrs dfg curri = + let i, curr = curri in + let dst_dep dst = + let dep_list = find_all_next_dst_read i dst 0 (take i instrs |> List.rev) + |> List.map (function (d, d') -> (i - d' - 1, d)) + in + List.fold_left (fun g -> + function (d, d') -> DFG.add_edge g (gen_vertex instrs d) (gen_vertex instrs d')) dfg dep_list + in + match curr with + | RBop (_, _, _, dst) -> dst_dep dst + | RBload (_, _, _, _, dst) -> dst_dep dst + | _ -> dfg + +let assigned_vars vars = function + | RBnop -> vars + | RBop (_, _, _, dst) -> dst :: vars + | RBload (_, _, _, _, dst) -> dst :: vars + | RBstore (_, _, _, _, _) -> vars + | RBsetpred (_, _, _) -> vars + +let get_pred = function + | RBnop -> None + | RBop (op, _, _, _) -> op + | RBload (op, _, _, _, _) -> op + | RBstore (op, _, _, _, _) -> op + | RBsetpred (_, _, _) -> None + +let independant_pred p p' = + match sat_pred_simple (Nat.of_int 100000) (Pand (p, p')) with + | Some None -> true + | _ -> false + +let check_dependent op1 op2 = + match op1, op2 with + | Some p, Some p' -> not (independant_pred p p') + | _, _ -> true + +let remove_unnecessary_deps graph = + let is_dependent v1 v2 g = + let (_, instr1) = v1 in + let (_, instr2) = v2 in + if check_dependent (get_pred instr1) (get_pred instr2) + then g + else DFG.remove_edge g v1 v2 + in + DFG.fold_edges is_dependent graph graph + +(** All the nodes in the DFG have to come after the source of the basic block, and should terminate + before the sink of the basic block. After that, there should be constraints for data + dependencies between nodes. *) +let gather_bb_constraints debug bb = + let ibody = List.mapi (fun i a -> (i, a)) bb.bb_body in + let dfg = List.fold_left (fun dfg v -> DFG.add_vertex dfg v) DFG.empty ibody in + let _, _, dfg' = + List.fold_left (accumulate_RAW_deps ibody) + (0, PTree.empty, dfg) + bb.bb_body + in + let dfg'' = List.fold_left (fun dfg f -> List.fold_left (f bb.bb_body) dfg ibody) dfg' + [ accumulate_WAW_deps; + accumulate_WAR_deps; + accumulate_RAW_mem_deps; + accumulate_WAR_mem_deps; + accumulate_WAW_mem_deps; + accumulate_RAW_pred_deps; + accumulate_WAR_pred_deps; + accumulate_WAW_pred_deps + ] + in + let dfg''' = remove_unnecessary_deps dfg'' in + (List.length bb.bb_body, dfg''', successors_instr bb.bb_exit) + +let encode_var bbn n i = { sv_type = VarType (bbn, n); sv_num = i } +let encode_bb bbn i = { sv_type = BBType bbn; sv_num = i } + +let add_super_nodes n dfg = + DFG.fold_vertex (function v1 -> fun g -> + (if DFG.in_degree dfg v1 = 0 + then G.add_edge_e g (encode_bb n 0, 0, encode_var n (fst v1) 0) + else g) |> + (fun g' -> + if DFG.out_degree dfg v1 = 0 + then G.add_edge_e g' (encode_var n (fst v1) 0, 0, encode_bb n 1) + else g')) dfg + +let add_data_deps n = + DFG.fold_edges_e (function ((i1, _), l, (i2, _)) -> fun g -> + G.add_edge_e g (encode_var n i1 0, 0, encode_var n i2 0) + ) + +let add_ctrl_deps n succs constr = + List.fold_left (fun g n' -> + G.add_edge_e g (encode_bb n 1, -1, encode_bb n' 0) + ) constr succs + +module BFDFG = Graph.Path.BellmanFord(DFG)(struct + include DFG + type t = int + let weight = DFG.E.label + let compare = compare + let add = (+) + let zero = 0 + end) + +module TopoDFG = Graph.Topological.Make(DFG) + +let negate_graph constr = + DFG.fold_edges_e (function (v1, e, v2) -> fun g -> + DFG.add_edge_e g (v1, -e, v2) + ) constr DFG.empty + +let add_cycle_constr max n dfg constr = + let negated_dfg = negate_graph dfg in + let longest_path v = BFDFG.all_shortest_paths negated_dfg v + |> BFDFG.H.to_seq |> List.of_seq in + let constrained_paths = List.filter (function (v, m) -> - m > max) in + List.fold_left (fun g -> function (v, v', w) -> + G.add_edge_e g (encode_var n (fst v) 0, + - (int_of_float (Float.ceil (Float.div (float_of_int w) (float_of_int max))) - 1), + encode_var n (fst v') 0) + ) constr (DFG.fold_vertex (fun v l -> + List.append l (longest_path v |> constrained_paths + |> List.map (function (v', w) -> (v, v', - w))) + ) dfg []) + +type resource = + | Mem + | SDiv + | UDiv + +type resources = { + res_mem: DFG.V.t list; + res_udiv: DFG.V.t list; + res_sdiv: DFG.V.t list; +} + +let find_resource = function + | RBload _ -> Some Mem + | RBstore _ -> Some Mem + | RBop (_, op, _, _) -> + ( match op with + | Odiv -> Some SDiv + | Odivu -> Some UDiv + | Omod -> Some SDiv + | Omodu -> Some UDiv + | _ -> None ) + | _ -> None + +let add_resource_constr n dfg constr = + let res = TopoDFG.fold (function (i, instr) -> + function {res_mem = ml; res_sdiv = sdl; res_udiv = udl} as r -> + match find_resource instr with + | Some SDiv -> {r with res_sdiv = (i, instr) :: sdl} + | Some UDiv -> {r with res_udiv = (i, instr) :: udl} + | Some Mem -> {r with res_mem = (i, instr) :: ml} + | None -> r + ) dfg {res_mem = []; res_sdiv = []; res_udiv = []} + in + let get_constraints l g = List.fold_left (fun gv v' -> + match gv with + | (g, None) -> (g, Some v') + | (g, Some v) -> + (G.add_edge_e g (encode_var n (fst v) 0, -1, encode_var n (fst v') 0), Some v') + ) (g, None) l |> fst + in + get_constraints (List.rev res.res_mem) constr + |> get_constraints (List.rev res.res_udiv) + |> get_constraints (List.rev res.res_sdiv) + +let gather_cfg_constraints c constr curr = + let (n, dfg) = curr in + match PTree.get (P.of_int n) c with + | None -> assert false + | Some { bb_exit = ctrl; _ } -> + add_super_nodes n dfg constr + |> add_data_deps n dfg + |> add_ctrl_deps n (successors_instr ctrl + |> List.map P.to_int + |> List.filter (fun n' -> n' < n)) + |> add_cycle_constr 8 n dfg + |> add_resource_constr n dfg + +let rec intersperse s = function + | [] -> [] + | [ a ] -> [ a ] + | x :: xs -> x :: s :: intersperse s xs + +let print_objective constr = + let vars = G.fold_vertex (fun v1 l -> + match v1 with + | { sv_type = VarType _; sv_num = 0 } -> print_sv v1 :: l + | _ -> l + ) constr [] + in + "min: " ^ String.concat "" (intersperse " + " vars) ^ ";\n" + +let print_lp constr = + print_objective constr ^ + (G.fold_edges_e (function (e1, w, e2) -> fun s -> + s ^ sprintf "%s - %s <= %d;\n" (print_sv e1) (print_sv e2) w + ) constr "" |> + G.fold_vertex (fun v1 s -> + s ^ sprintf "int %s;\n" (print_sv v1) + ) constr) + +let update_schedule v = function Some l -> Some (v :: l) | None -> Some [ v ] + +let parse_soln tree s = + let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in + if Str.string_match r s 0 then + IMap.update + (Str.matched_group 1 s |> int_of_string) + (update_schedule + ( Str.matched_group 2 s |> int_of_string, + Str.matched_group 3 s |> int_of_string )) + tree + else tree + +let solve_constraints constr = + let oc = open_out "lpsolve.txt" in + fprintf oc "%s\n" (print_lp constr); + close_out oc; + + Str.split (Str.regexp_string "\n") (read_process "lp_solve lpsolve.txt") + |> drop 3 + |> List.fold_left parse_soln IMap.empty + +let subgraph dfg l = + let dfg' = List.fold_left (fun g v -> DFG.add_vertex g v) DFG.empty l in + List.fold_left (fun g v -> + List.fold_left (fun g' v' -> + let edges = DFG.find_all_edges dfg v v' in + List.fold_left DFG.add_edge_e g' edges + ) g l + ) dfg' l + +let rec all_successors dfg v = + List.concat (List.fold_left (fun l v -> + all_successors dfg v :: l + ) [] (DFG.succ dfg v)) + +let order_instr dfg = + DFG.fold_vertex (fun v li -> + if DFG.in_degree dfg v = 0 + then (List.map snd (v :: all_successors dfg v)) :: li + else li + ) dfg [] + +let combine_bb_schedule schedule s = + let i, st = s in + IMap.update st (update_schedule i) schedule + +(**let add_el dfg i l = + List.*) + +let check_in el = + List.exists (List.exists ((=) el)) + +let all_dfs dfg = + let roots = DFG.fold_vertex (fun v li -> + if DFG.in_degree dfg v = 0 then v :: li else li + ) dfg [] in + let dfg' = DFG.fold_edges (fun v1 v2 g -> DFG.add_edge g v2 v1) dfg dfg in + List.fold_left (fun a el -> + if check_in el a then a else + (DFGDfs.fold_component (fun v l -> v :: l) [] dfg' el) :: a) [] roots + +(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *) +let transf_rtlpar c c' (schedule : (int * int) list IMap.t) = + let f i bb : RTLPar.bblock = + match bb with + | { bb_body = []; bb_exit = c } -> { bb_body = []; bb_exit = c } + | { bb_body = bb_body'; bb_exit = ctrl_flow } -> + let dfg = match PTree.get i c' with None -> assert false | Some x -> x in + let i_sched = IMap.find (P.to_int i) schedule in + let i_sched_tree = + List.fold_left combine_bb_schedule IMap.empty i_sched + in + let body = IMap.to_seq i_sched_tree |> List.of_seq |> List.map snd + |> List.map (List.map (fun x -> (x, List.nth bb_body' x))) + in + (*let final_body = List.map (fun x -> subgraph dfg x |> order_instr) body in*) + let final_body2 = List.map (fun x -> subgraph dfg x + |> (fun x -> + all_dfs x + |> List.map (subgraph x) + |> List.map (fun y -> + TopoDFG.fold (fun i l -> snd i :: l) y [] + |> List.rev))) body + in + { bb_body = final_body2; + bb_exit = ctrl_flow + } + in + PTree.map f c + +let schedule entry (c : RTLBlock.bb RTLBlockInstr.code) = + let debug = true in + let transf_graph (_, dfg, _) = dfg in + let c' = PTree.map1 (fun x -> gather_bb_constraints false x |> transf_graph) c in + (*let _ = if debug then PTree.map (fun r o -> printf "##### %d #####\n%a\n\n" (P.to_int r) print_dfg o) c' else PTree.empty in*) + let cgraph = PTree.elements c' + |> List.map (function (x, y) -> (P.to_int x, y)) + |> List.fold_left (gather_cfg_constraints c) G.empty + in + let graph = open_out "constr_graph.dot" in + fprintf graph "%a\n" GDot.output_graph cgraph; + close_out graph; + let schedule' = solve_constraints cgraph in + (**IMap.iter (fun a b -> printf "##### %d #####\n%a\n\n" a (print_list print_tuple) b) schedule';*) + (**printf "Schedule: %a\n" (fun a x -> IMap.iter (fun d -> fprintf a "%d: %a\n" d (print_list print_tuple)) x) schedule';*) + transf_rtlpar c c' schedule' + +let rec find_reachable_states c e = + match PTree.get e c with + | Some { bb_exit = ex; _ } -> + e :: List.fold_left (fun x a -> List.concat [x; find_reachable_states c a]) [] + (successors_instr ex |> List.filter (fun x -> P.lt x e)) + | None -> assert false + +let add_to_tree c nt i = + match PTree.get i c with + | Some p -> PTree.set i p nt + | None -> assert false + +let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function = + let scheduled = schedule f.fn_entrypoint f.fn_code in + let reachable = find_reachable_states scheduled f.fn_entrypoint + |> List.to_seq |> SS.of_seq |> SS.to_seq |> List.of_seq in + { fn_sig = f.fn_sig; + fn_params = f.fn_params; + fn_stacksize = f.fn_stacksize; + fn_code = List.fold_left (add_to_tree scheduled) PTree.empty reachable; + fn_entrypoint = f.fn_entrypoint + } diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v index 0df8b7e..39504a2 100644 --- a/src/hls/Verilog.v +++ b/src/hls/Verilog.v @@ -428,7 +428,7 @@ Inductive expr_runp : fext -> assocmap -> assocmap_arr -> expr -> value -> Prop expr_runp fext reg stack fs vf -> valueToBool vc = false -> expr_runp fext reg stack (Vternary c ts fs) vf. -Hint Constructors expr_runp : verilog. +#[export] Hint Constructors expr_runp : verilog. Definition handle_opt {A : Type} (err : errmsg) (val : option A) : res A := @@ -526,7 +526,7 @@ Inductive stmnt_runp: fext -> reg_associations -> arr_associations -> stmnt_runp f asr asa (Vnonblock lhs rhs) asr (nonblock_arr r i asa rhsval). -Hint Constructors stmnt_runp : verilog. +#[export] Hint Constructors stmnt_runp : verilog. Inductive mi_stepp : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := @@ -540,7 +540,7 @@ Inductive mi_stepp : fext -> reg_associations -> arr_associations -> | mi_stepp_Vdecl : forall f sr0 sa0 d, mi_stepp f sr0 sa0 (Vdeclaration d) sr0 sa0. -Hint Constructors mi_stepp : verilog. +#[export] Hint Constructors mi_stepp : verilog. Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> module_item -> reg_associations -> arr_associations -> Prop := @@ -554,7 +554,7 @@ Inductive mi_stepp_negedge : fext -> reg_associations -> arr_associations -> | mi_stepp_negedge_Vdecl : forall f sr0 sa0 d, mi_stepp_negedge f sr0 sa0 (Vdeclaration d) sr0 sa0. -Hint Constructors mi_stepp : verilog. +#[export] Hint Constructors mi_stepp : verilog. Inductive mis_stepp : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := @@ -566,7 +566,7 @@ Inductive mis_stepp : fext -> reg_associations -> arr_associations -> | mis_stepp_Nil : forall f sr sa, mis_stepp f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. +#[export] Hint Constructors mis_stepp : verilog. Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> list module_item -> reg_associations -> arr_associations -> Prop := @@ -578,7 +578,7 @@ Inductive mis_stepp_negedge : fext -> reg_associations -> arr_associations -> | mis_stepp_negedge_Nil : forall f sr sa, mis_stepp_negedge f sr sa nil sr sa. -Hint Constructors mis_stepp : verilog. +#[export] Hint Constructors mis_stepp : verilog. Local Close Scope error_monad_scope. @@ -634,7 +634,7 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop := mst = mod_st m -> step g (Returnstate (Stackframe r m pc asr asa :: sf) i) Events.E0 (State sf m pc ((asr # mst <- (posToValue pc)) # r <- i) asa). -Hint Constructors step : verilog. +#[export] Hint Constructors step : verilog. Inductive initial_state (p: program): state -> Prop := | initial_state_intro: forall b m0 m, @@ -692,7 +692,7 @@ Proof. learn (H1 _ H2) end; crush). Qed. -Hint Resolve expr_runp_determinate : verilog. +#[export] Hint Resolve expr_runp_determinate : verilog. Lemma location_is_determinate : forall f asr asa e l, @@ -741,7 +741,7 @@ Lemma stmnt_runp_determinate : learn (H1 _ _ H2) end; crush). Qed. -Hint Resolve stmnt_runp_determinate : verilog. +#[export] Hint Resolve stmnt_runp_determinate : verilog. Lemma mi_stepp_determinate : forall f asr0 asa0 m asr1 asa1, diff --git a/src/hls/Veriloggenproof.v b/src/hls/Veriloggenproof.v index 8ecab63..37b4dfd 100644 --- a/src/hls/Veriloggenproof.v +++ b/src/hls/Veriloggenproof.v @@ -387,7 +387,7 @@ Section CORRECTNESS. Lemma symbols_preserved: forall (s: AST.ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intros. eapply (Genv.find_symbol_match TRANSL). Qed. - Hint Resolve symbols_preserved : verilogproof. + #[local] Hint Resolve symbols_preserved : verilogproof. (* Lemma function_ptr_translated: *) (* forall (b: Values.block) (f: HTL.fundef), *) diff --git a/test/Makefile b/test/Makefile new file mode 100644 index 0000000..9413c70 --- /dev/null +++ b/test/Makefile @@ -0,0 +1,34 @@ +CC ?= gcc +VERICERT ?= vericert +VERICERT_OPTS ?= -fschedule +IVERILOG ?= iverilog +IVERILOG_OPTS ?= + +TESTS := $(patsubst %.c,%.check,$(wildcard *.c)) + +all: $(TESTS) + +%.gcc.out: %.gcc + @./$< ; echo "$$?" >$@ + +%.o: %.c + @$(CC) $(CFLAGS) -c -o $@ $< + +%.gcc: %.o + @$(CC) $(CFLAGS) -o $@ $< + +%.v: %.c + @$(VERICERT) $(VERICERT_OPTS) -o $@ $< + +%.iver: %.v + @$(IVERILOG) $(IVERILOG_OPTS) -o $@ -- $< + +%.veri.out: %.iver + @./$< | tail -n1 | sed -r -e 's/[^0-9]*([0-9]+)/\1/' >$@ + +%.check: %.gcc.out %.veri.out + @diff $^ >$@ + @printf "\033[0;36mOK\033[0m\t$(patsubst %.check,%,$@)\n" + +clean: + rm -f *.check *.gcc *.gcc.out *.o *.v *.iver *.veri.out diff --git a/test/test_all.sh b/test/test_all.sh index f072eba..f2b045b 100755 --- a/test/test_all.sh +++ b/test/test_all.sh @@ -1,3 +1,5 @@ +#!/bin/bash + mytmpdir=$(mktemp -d 2>/dev/null || mktemp -d -t 'mytmpdir') echo "--------------------------------------------------" echo "Created working directory: $mytmpdir" @@ -31,7 +33,7 @@ for cfile in $test_dir/*.c; do gcc -o $outbase.gcc $cfile >/dev/null 2>&1 $outbase.gcc expected=$? - vericert -drtl -o $outbase.v $cfile >/dev/null 2>&1 + vericert -fschedule -drtl -o $outbase.v $cfile >/dev/null 2>&1 if [[ ! -f $outbase.v ]]; then echo "ERROR" continue |