aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2021-10-18 17:05:46 +0100
committerYann Herklotz <git@yannherklotz.com>2021-10-18 17:05:46 +0100
commitfbfa988072ce2eba808b9a6631af5f8e86cd9df0 (patch)
tree5146e558d5c9c6e9a399225eed0784b8dc12558f
parent603768a49eac2005729dd03e723ff6c5a6b292f7 (diff)
parentfe06668f0de56635efe55310d7a64289a37c1d90 (diff)
downloadvericert-dev/michalis.tar.gz
vericert-dev/michalis.zip
Merge branch 'master' into dev/michalisdev/michalis
-rw-r--r--.gitignore68
-rw-r--r--CHANGELOG.org49
-rw-r--r--CITATION.cff4
-rw-r--r--Makefile3
-rw-r--r--README.org29
-rw-r--r--benchmarks/polybench-syn/common.mk2
-rw-r--r--default.nix10
m---------docs0
-rw-r--r--driver/VericertDriver.ml6
-rw-r--r--src/Compiler.v12
-rw-r--r--src/VericertClflags.ml1
-rw-r--r--src/common/Monad.v4
-rw-r--r--src/common/Vericertlib.v8
-rw-r--r--src/extraction/Extraction.v9
-rw-r--r--src/hls/Abstr.v973
-rw-r--r--src/hls/Array.v10
-rw-r--r--src/hls/AssocMap.v52
-rw-r--r--src/hls/FunctionalUnits.v76
-rw-r--r--src/hls/HTL.v2
-rw-r--r--src/hls/HTLPargen.v27
-rw-r--r--src/hls/HTLgen.v14
-rw-r--r--src/hls/HTLgenproof.v43
-rw-r--r--src/hls/HTLgenspec.v20
-rw-r--r--src/hls/HashTree.v438
-rw-r--r--src/hls/IfConversion.v2
-rw-r--r--src/hls/Memorygen.v150
-rw-r--r--src/hls/Partition.ml124
-rw-r--r--src/hls/PrintExpression.ml40
-rw-r--r--src/hls/PrintHTL.ml6
-rw-r--r--src/hls/PrintRTLBlock.ml72
-rw-r--r--src/hls/PrintRTLBlockInstr.ml87
-rw-r--r--src/hls/PrintRTLPar.ml74
-rw-r--r--src/hls/RTLBlock.v15
-rw-r--r--src/hls/RTLBlockInstr.v161
-rw-r--r--src/hls/RTLPar.v15
-rw-r--r--src/hls/RTLPargen.v1366
-rw-r--r--src/hls/RTLPargenproof.v161
-rw-r--r--src/hls/Sat.v28
-rw-r--r--src/hls/Schedule.ml831
-rw-r--r--src/hls/Verilog.v18
-rw-r--r--src/hls/Veriloggenproof.v2
-rw-r--r--test/Makefile34
-rwxr-xr-xtest/test_all.sh4
43 files changed, 4239 insertions, 811 deletions
diff --git a/.gitignore b/.gitignore
index 70f1a7e..0d73417 100644
--- a/.gitignore
+++ b/.gitignore
@@ -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
diff --git a/Makefile b/Makefile
index d14ef13..0749d1c 100644
--- a/Makefile
+++ b/Makefile
@@ -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::
diff --git a/README.org b/README.org
index 4426561..cf8bd34 100644
--- a/README.org
+++ b/README.org
@@ -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>&nbsp;<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