aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile9
-rw-r--r--default.nix4
-rw-r--r--docs/basic-block-generation.org497
-rw-r--r--docs/scheduler-languages.org682
-rw-r--r--docs/scheduler.org2317
-rw-r--r--src/Compiler.v115
-rw-r--r--src/bourdoncle/Bourdoncle.v4
-rw-r--r--src/common/Maps.v5
-rw-r--r--src/hls/Abstr.v54
-rw-r--r--src/hls/Array.v5
-rw-r--r--src/hls/HTL.v16
-rw-r--r--src/hls/HTLPargen.v5
-rw-r--r--src/hls/HTLgenproof.v39
-rw-r--r--src/hls/HTLgenspec.v10
-rw-r--r--src/hls/IfConversion.v12
-rw-r--r--src/hls/RICtransf.v14
-rw-r--r--src/hls/RTLBlock.v47
-rw-r--r--src/hls/RTLBlockInstr.v142
-rw-r--r--src/hls/RTLBlockgen.v15
-rw-r--r--src/hls/RTLBlockgenproof.v38
-rw-r--r--src/hls/RTLPar.v40
-rw-r--r--src/hls/RTLPargen.v104
-rw-r--r--src/hls/RTLPargenproof.v15
-rw-r--r--src/hls/Schedule.ml2
-rw-r--r--src/hls/ValueInt.v42
-rw-r--r--src/hls/Verilog.v119
26 files changed, 582 insertions, 3770 deletions
diff --git a/Makefile b/Makefile
index de3c3b7..a6aa914 100644
--- a/Makefile
+++ b/Makefile
@@ -17,6 +17,7 @@ COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
COQMAKE := $(COQBIN)coq_makefile
COQDOCFLAGS := --no-lib-name -l
+ALECTRYON_OPTS := --html-minification --long-line-threshold 80 --coq-driver sertop_noexec $(COQINCLUDES)
VS := src/Compiler.v src/Simulator.v src/HLSOpts.v $(foreach d, common hls bourdoncle, $(wildcard src/$(d)/*.v))
LIT := docs/basic-block-generation.org docs/scheduler.org docs/scheduler-languages.org
@@ -48,7 +49,13 @@ proof: Makefile.coq
$(MAKE) -f Makefile.coq
@rm -f src/extraction/STAMP
-doc: Makefile.coq
+doc-html: $(patsubst src/%.v,html/%.html,$(VS))
+
+html/%.html: src/%.v
+ @mkdir -p $(dir $@)
+ @echo "ALECTRYON" $@; alectryon $(ALECTRYON_OPTS) $< -o $@
+
+coqdoc: Makefile.coq
$(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq html
cp ./docs/res/coqdoc.css html/.
diff --git a/default.nix b/default.nix
index e3ce09b..eb1125c 100644
--- a/default.nix
+++ b/default.nix
@@ -11,6 +11,10 @@ stdenv.mkDerivation {
ncoq.ocaml ncoq.ocamlPackages.findlib ncoq.ocamlPackages.menhir
ncoq.ocamlPackages.ocamlgraph ncoq.ocamlPackages.merlin
ncoq.ocamlPackages.menhirLib
+
+ ncoqPackages.serapi
+ python3
+ python3Packages.alectryon
];
enableParallelBuilding = true;
diff --git a/docs/basic-block-generation.org b/docs/basic-block-generation.org
deleted file mode 100644
index 1d78dad..0000000
--- a/docs/basic-block-generation.org
+++ /dev/null
@@ -1,497 +0,0 @@
-#+title: Basic Block Generation
-#+author: Yann Herklotz
-#+email: yann [at] yannherklotz [dot] com
-
-* RTLBlockgen
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgen.v
-:END:
-
-Refers to [[rtlblockgen-equalities][rtlblockgen-equalities]].
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: rtlblockgen-imports
-#+begin_src coq
-Require compcert.backend.RTL.
-Require Import compcert.common.AST.
-Require Import compcert.lib.Maps.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Floats.
-
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLBlock.
-
-#[local] Open Scope positive.
-#+end_src
-
-#+name: rtlblockgen-equalities-insert
-#+begin_src coq :comments no
-<<rtlblockgen-equalities>>
-#+end_src
-
-#+name: rtlblockgen-main
-#+begin_src coq
-Parameter partition : RTL.function -> Errors.res function.
-
-(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold
- function to find the desired element. *)
-Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive :=
- List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes).
-
-(*Compute find_block (2::94::28::40::19::nil) 40.*)
-
-Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) :=
- match istr, istr' with
- | RTL.Inop n', RBnop => (n' + 1 =? n)
- | RTL.Iop op args dst n', RBop None op' args' dst' =>
- ceq operation_eq op op' &&
- ceq list_pos_eq args args' &&
- ceq peq dst dst' && (n' + 1 =? n)
- | RTL.Iload chunk addr args dst n', RBload None chunk' addr' args' dst' =>
- ceq memory_chunk_eq chunk chunk' &&
- ceq addressing_eq addr addr' &&
- ceq list_pos_eq args args' &&
- ceq peq dst dst' &&
- (n' + 1 =? n)
- | RTL.Istore chunk addr args src n', RBstore None chunk' addr' args' src' =>
- ceq memory_chunk_eq chunk chunk' &&
- ceq addressing_eq addr addr' &&
- ceq list_pos_eq args args' &&
- ceq peq src src' &&
- (n' + 1 =? n)
- | _, _ => false
- end.
-
-Definition check_cf_instr_body (istr: RTL.instruction) (istr': instr): bool :=
- match istr, istr' with
- | RTL.Iop op args dst _, RBop None op' args' dst' =>
- ceq operation_eq op op' &&
- ceq list_pos_eq args args' &&
- ceq peq dst dst'
- | RTL.Iload chunk addr args dst _, RBload None chunk' addr' args' dst' =>
- ceq memory_chunk_eq chunk chunk' &&
- ceq addressing_eq addr addr' &&
- ceq list_pos_eq args args' &&
- ceq peq dst dst'
- | RTL.Istore chunk addr args src _, RBstore None chunk' addr' args' src' =>
- ceq memory_chunk_eq chunk chunk' &&
- ceq addressing_eq addr addr' &&
- ceq list_pos_eq args args' &&
- ceq peq src src'
- | RTL.Inop _, RBnop
- | RTL.Icall _ _ _ _ _, RBnop
- | RTL.Itailcall _ _ _, RBnop
- | RTL.Ibuiltin _ _ _ _, RBnop
- | RTL.Icond _ _ _ _, RBnop
- | RTL.Ijumptable _ _, RBnop
- | RTL.Ireturn _, RBnop => true
- | _, _ => false
- end.
-
-Definition check_cf_instr (istr: RTL.instruction) (istr': cf_instr) :=
- match istr, istr' with
- | RTL.Inop n, RBgoto n' => (n =? n')
- | RTL.Iop _ _ _ n, RBgoto n' => (n =? n')
- | RTL.Iload _ _ _ _ n, RBgoto n' => (n =? n')
- | RTL.Istore _ _ _ _ n, RBgoto n' => (n =? n')
- | RTL.Icall sig (inl r) args dst n, RBcall sig' (inl r') args' dst' n' =>
- ceq signature_eq sig sig' &&
- ceq peq r r' &&
- ceq list_pos_eq args args' &&
- ceq peq dst dst' &&
- (n =? n')
- | RTL.Icall sig (inr i) args dst n, RBcall sig' (inr i') args' dst' n' =>
- ceq signature_eq sig sig' &&
- ceq peq i i' &&
- ceq list_pos_eq args args' &&
- ceq peq dst dst' &&
- (n =? n')
- | RTL.Itailcall sig (inl r) args, RBtailcall sig' (inl r') args' =>
- ceq signature_eq sig sig' &&
- ceq peq r r' &&
- ceq list_pos_eq args args'
- | RTL.Itailcall sig (inr r) args, RBtailcall sig' (inr r') args' =>
- ceq signature_eq sig sig' &&
- ceq peq r r' &&
- ceq list_pos_eq args args'
- | RTL.Icond cond args n1 n2, RBcond cond' args' n1' n2' =>
- ceq condition_eq cond cond' &&
- ceq list_pos_eq args args' &&
- ceq peq n1 n1' && ceq peq n2 n2'
- | RTL.Ijumptable r ns, RBjumptable r' ns' =>
- ceq peq r r' && ceq list_pos_eq ns ns'
- | RTL.Ireturn (Some r), RBreturn (Some r') =>
- ceq peq r r'
- | RTL.Ireturn None, RBreturn None => true
- | _, _ => false
- end.
-
-Definition is_cf_instr (n: positive) (i: RTL.instruction) :=
- match i with
- | RTL.Inop n' => negb (n' + 1 =? n)
- | RTL.Iop _ _ _ n' => negb (n' + 1 =? n)
- | RTL.Iload _ _ _ _ n' => negb (n' + 1 =? n)
- | RTL.Istore _ _ _ _ n' => negb (n' + 1 =? n)
- | RTL.Icall _ _ _ _ _ => true
- | RTL.Itailcall _ _ _ => true
- | RTL.Ibuiltin _ _ _ _ => true
- | RTL.Icond _ _ _ _ => true
- | RTL.Ijumptable _ _ => true
- | RTL.Ireturn _ => true
- end.
-
-Definition check_present_blocks (c: code) (n: list positive) (max: positive) (i: positive) (istr: RTL.instruction) :=
- let blockn := find_block max n i in
- match c ! blockn with
- | Some istrs =>
- match List.nth_error istrs.(bb_body) (Pos.to_nat blockn - Pos.to_nat i)%nat with
- | Some istr' =>
- if is_cf_instr i istr
- then check_cf_instr istr istrs.(bb_exit) && check_cf_instr_body istr istr'
- else check_instr i istr istr'
- | None => false
- end
- | None => false
- end.
-
-Definition transl_function (f: RTL.function) :=
- match partition f with
- | Errors.OK f' =>
- let blockids := map fst (PTree.elements f'.(fn_code)) in
- if forall_ptree (check_present_blocks f'.(fn_code) blockids (fold_right Pos.max 1 blockids))
- f.(RTL.fn_code) then
- Errors.OK f'
- else Errors.Error (Errors.msg "check_present_blocks failed")
- | Errors.Error msg => Errors.Error msg
- end.
-
-Definition transl_fundef := transf_partial_fundef transl_function.
-
-Definition transl_program : RTL.program -> Errors.res program :=
- transform_partial_program transl_fundef.
-#+end_src
-
-** Equalities
-
-#+name: rtlblockgen-equalities
-#+begin_src coq :tangle no
-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_pos_eq : forall (x y : list positive), {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_pos_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_pos_eq; intro.
- generalize AST.ident_eq; intro.
- repeat decide equality.
-Defined.
-
-Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
- if eqd a b then true else false.
-#+end_src
-
-* RTLBlockgenproof
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockgenproof.v
-:END:
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-** Imports
-
-#+name: rtlblockgenproof-imports
-#+begin_src coq
-Require compcert.backend.RTL.
-Require Import compcert.common.AST.
-Require Import compcert.lib.Maps.
-
-Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLBlockgen.
-#+end_src
-
-** Match states
-
-The ~match_states~ predicate describes which states are equivalent between the two languages, in this
-case ~RTL~ and ~RTLBlock~.
-
-#+name: rtlblockgenproof-match-states
-#+begin_src coq
-Inductive match_states : RTL.state -> RTLBlock.state -> Prop :=
-| match_state :
- forall stk f tf sp pc rs m
- (TF: transl_function f = OK tf),
- match_states (RTL.State stk f sp pc rs m)
- (RTLBlock.State stk tf sp (find_block max n i) rs m).
-#+end_src
-
-** Correctness
-
-#+name: rtlblockgenproof-correctness
-#+begin_src coq
-Section CORRECTNESS.
-
- Context (prog : RTL.program).
- Context (tprog : RTLBlock.program).
-
- Context (TRANSL : match_prog prog tprog).
-
- Theorem transf_program_correct:
- Smallstep.forward_simulation (RTL.semantics prog) (RTLBlock.semantics tprog).
- Proof.
- eapply Smallstep.forward_simulation_plus; eauto with htlproof.
- apply senv_preserved.
-
-End CORRECTNESS.
-#+end_src
-
-* Partition
-:PROPERTIES:
-:header-args:ocaml: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/Partition.ml
-:END:
-
-#+begin_src ocaml :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: partition-main
-#+begin_src ocaml
-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 = [RBnop]; bb_exit = RBgoto s }
- else
- Errors.OK { bb_body = [RBnop]; 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 = [RBnop]; 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
-#+end_src
-
-* License
-
-#+name: license
-#+begin_src coq :tangle no
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2022 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/>.
- *)
-#+end_src
diff --git a/docs/scheduler-languages.org b/docs/scheduler-languages.org
deleted file mode 100644
index 02249f8..0000000
--- a/docs/scheduler-languages.org
+++ /dev/null
@@ -1,682 +0,0 @@
-#+title: Scheduler Languages
-#+author: Yann Herklotz
-#+email: yann [at] yannherklotz [dot] com
-
-* RTLBlockInstr
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlockInstr.v
-:END:
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: rtlblockinstr-imports
-#+begin_src coq
-Require Import Coq.micromega.Lia.
-
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Events.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-Require Import compcert.verilog.Op.
-
-Require Import Predicate.
-Require Import Vericertlib.
-#+end_src
-
-These instructions are used for ~RTLBlock~ and ~RTLPar~, so that they have consistent instructions,
-which greatly simplifies the proofs, as they will by default have the same instruction syntax and
-semantics. The only changes are therefore at the top-level of the instructions.
-
-** Instruction Definition
-
-First, we define the instructions that can be placed into a basic block, meaning they won't branch.
-The main changes to how instructions are defined in [RTL], is that these instructions don't have a
-next node, as they will be in a basic block, and they also have an optional predicate ([pred_op]).
-
-#+name: rtlblockinstr-instr-def
-#+begin_src coq
-Definition node := positive.
-
-Inductive instr : Type :=
-| RBnop : instr
-| RBop : option pred_op -> operation -> list reg -> reg -> instr
-| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
-#+end_src
-
-** Control-Flow Instruction Definition
-
-These are the instructions that count as control-flow, and will be placed at the end of the basic
-blocks.
-
-#+name: rtlblockinstr-cf-instr-def
-#+begin_src coq
-Inductive cf_instr : Type :=
-| RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
-| RBtailcall : signature -> reg + ident -> list reg -> cf_instr
-| RBbuiltin : external_function -> list (builtin_arg reg) ->
- builtin_res reg -> node -> cf_instr
-| RBcond : condition -> list reg -> node -> node -> cf_instr
-| RBjumptable : reg -> list node -> cf_instr
-| RBreturn : option reg -> cf_instr
-| RBgoto : node -> cf_instr
-| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
-#+end_src
-
-** Helper functions
-
-#+name: rtlblockinstr-helpers
-#+begin_src coq
-Fixpoint successors_instr (i : cf_instr) : list node :=
- match i with
- | RBcall sig ros args res s => s :: nil
- | RBtailcall sig ros args => nil
- | RBbuiltin ef args res s => s :: nil
- | RBcond cond args ifso ifnot => ifso :: ifnot :: nil
- | RBjumptable arg tbl => tbl
- | RBreturn optarg => nil
- | RBgoto n => n :: nil
- | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
- end.
-
-Definition max_reg_instr (m: positive) (i: instr) :=
- match i with
- | RBnop => m
- | RBop p op args res =>
- fold_left Pos.max args (Pos.max res m)
- | RBload p chunk addr args dst =>
- fold_left Pos.max args (Pos.max dst m)
- | RBstore p chunk addr args src =>
- fold_left Pos.max args (Pos.max src m)
- | RBsetpred p' c args p =>
- fold_left Pos.max args m
- end.
-
-Fixpoint max_reg_cfi (m : positive) (i : cf_instr) :=
- match i with
- | RBcall sig (inl r) args res s =>
- fold_left Pos.max args (Pos.max r (Pos.max res m))
- | RBcall sig (inr id) args res s =>
- fold_left Pos.max args (Pos.max res m)
- | RBtailcall sig (inl r) args =>
- fold_left Pos.max args (Pos.max r m)
- | RBtailcall sig (inr id) args =>
- fold_left Pos.max args m
- | RBbuiltin ef args res s =>
- fold_left Pos.max (params_of_builtin_args args)
- (fold_left Pos.max (params_of_builtin_res res) m)
- | RBcond cond args ifso ifnot => fold_left Pos.max args m
- | RBjumptable arg tbl => Pos.max arg m
- | RBreturn None => m
- | RBreturn (Some arg) => Pos.max arg m
- | RBgoto n => m
- | RBpred_cf p c1 c2 => Pos.max (max_reg_cfi m c1) (max_reg_cfi m c2)
- end.
-
-Definition regset := Regmap.t val.
-Definition predset := PMap.t bool.
-
-Definition eval_predf (pr: predset) (p: pred_op) :=
- sat_predicate p (fun x => pr !! (Pos.of_nat x)).
-
-#[global]
-Instance eval_predf_Proper : Proper (eq ==> equiv ==> eq) eval_predf.
-Proof.
- unfold Proper. simplify. unfold "==>".
- intros.
- unfold sat_equiv in *. intros. unfold eval_predf. subst. apply H0.
-Qed.
-
-#[local] Open Scope pred_op.
-
-Lemma eval_predf_Pand :
- forall ps p p',
- eval_predf ps (p ∧ p') = eval_predf ps p && eval_predf ps p'.
-Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
-
-Lemma eval_predf_Por :
- forall ps p p',
- eval_predf ps (p ∨ p') = eval_predf ps p || eval_predf ps p'.
-Proof. unfold eval_predf; split; simplify; auto with bool. Qed.
-
-Lemma eval_predf_pr_equiv :
- forall p ps ps',
- (forall x, ps !! x = ps' !! x) ->
- eval_predf ps p = eval_predf ps' p.
-Proof.
- induction p; simplify; auto;
- try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
- [repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
- erewrite IHp1; try eassumption; erewrite IHp2; eauto.
-Qed.
-
-Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
- match rl, vl with
- | r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
- | _, _ => Regmap.init Vundef
- end.
-#+end_src
-
-*** Instruction State
-
-Definition of the instruction state, which contains the following:
-
-- ~is_rs~ :: This is the current state of the registers.
-- ~is_ps~ :: This is the current state of the predicate registers, which is in a separate namespace
- and area compared to the standard registers in [is_rs].
-- ~is_mem~ :: The current state of the memory.
-
-#+name: rtlblockinstr-instr-state
-#+begin_src coq
-Record instr_state := mk_instr_state {
- is_rs: regset;
- is_ps: predset;
- is_mem: mem;
-}.
-#+end_src
-
-** Top-Level Type Definitions
-
-#+name: rtlblockinstr-type-def
-#+begin_src coq
-Section DEFINITION.
-
- Context {bblock_body: Type}.
-
- Record bblock : Type := mk_bblock {
- bb_body: bblock_body;
- bb_exit: cf_instr
- }.
-
- Definition code: Type := PTree.t bblock.
-
- Record function: Type := mkfunction {
- fn_sig: signature;
- fn_params: list reg;
- fn_stacksize: Z;
- fn_code: code;
- fn_entrypoint: node
- }.
-
- Definition fundef := AST.fundef function.
-
- Definition program := AST.program fundef unit.
-
- Definition funsig (fd: fundef) :=
- match fd with
- | Internal f => fn_sig f
- | External ef => ef_sig ef
- end.
-
- Inductive stackframe : Type :=
- | Stackframe:
- forall (res: reg) (**r where to store the result *)
- (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 *)
- (pr: predset), (**r predicate state of the calling function *)
- stackframe.
-#+end_src
-
-*** State definition
-:PROPERTIES:
-:CUSTOM_ID: state
-:END:
-
-Definition of the ~state~ type, which is used by the ~step~ functions.
-
-#+name: rtlblockinstr-state
-#+begin_src coq
- Variant state : Type :=
- | State:
- forall (stack: list stackframe) (**r call stack *)
- (f: function) (**r current function *)
- (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:
- forall (stack: list stackframe) (**r call stack *)
- (f: fundef) (**r function to call *)
- (args: list val) (**r arguments to the call *)
- (m: mem), (**r memory state *)
- state
- | Returnstate:
- forall (stack: list stackframe) (**r call stack *)
- (v: val) (**r return value for the call *)
- (m: mem), (**r memory state *)
- state.
-#+end_src
-
-#+name: rtlblockinstr-state
-#+begin_src coq
-End DEFINITION.
-#+end_src
-
-** Semantics
-
-#+name: rtlblockinstr-semantics
-#+begin_src coq
-Section RELSEM.
-
- Context {bblock_body : Type}.
-
- Definition genv := Genv.t (@fundef bblock_body) unit.
-
- Context (ge: genv).
-
- Definition find_function
- (ros: reg + ident) (rs: regset) : option fundef :=
- match ros with
- | inl r => Genv.find_funct ge rs#r
- | inr symb =>
- match Genv.find_symbol ge symb with
- | None => None
- | Some b => Genv.find_funct_ptr ge b
- end
- end.
-
- Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
- | eval_pred_true:
- forall i i' p,
- eval_predf (is_ps i) p = true ->
- eval_pred (Some p) i i' i'
- | eval_pred_false:
- forall i i' p,
- eval_predf (is_ps i) p = false ->
- eval_pred (Some p) i i' i
- | eval_pred_none:
- forall i i', eval_pred None i i' i.
-#+end_src
-
-*** Step a single instruction
-:PROPERTIES:
-:CUSTOM_ID: step_instr
-:END:
-
-#+name: rtlblockinstr-step_instr
-#+begin_src coq
- Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
- | exec_RBnop:
- forall sp ist,
- step_instr sp ist RBnop ist
- | exec_RBop:
- 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 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 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 p' ist,
- Op.eval_condition c rs##args m = Some b ->
- eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
- step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist.
-#+end_src
-
-*** Step a control-flow instruction
-:PROPERTIES:
-:CUSTOM_ID: step_cf_instr
-:END:
-
-#+name: rtlblockinstr-step_cf_instr
-#+begin_src coq
- 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' pr,
- find_function ros rs = Some fd ->
- funsig fd = sig ->
- 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 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 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 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 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' 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 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' pr,
- rs#arg = Vint n ->
- list_nth_z tbl (Int.unsigned n) = Some pc' ->
- 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 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_src
-
-#+name: rtlblockinstr-end_RELSEM
-#+begin_src coq
-End RELSEM.
-#+end_src
-
-* RTLBlock
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLBlock.v
-:END:
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: rtlblock-main
-#+begin_src coq
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Events.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Smallstep.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Coqlib.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-Require Import compcert.verilog.Op.
-
-Require Import vericert.hls.RTLBlockInstr.
-
-Definition bb := list instr.
-
-Definition bblock := @bblock bb.
-Definition code := @code bb.
-Definition function := @function bb.
-Definition fundef := @fundef bb.
-Definition program := @program bb.
-Definition funsig := @funsig bb.
-Definition stackframe := @stackframe bb.
-Definition state := @state bb.
-
-Definition genv := @genv bb.
-#+end_src
-
-** Semantics
-
-We first describe the semantics by assuming a global program environment with type ~genv~ which was
-declared earlier.
-
-#+name: rtlblock-semantics
-#+begin_src coq
-Section RELSEM.
-
- Context (ge: genv).
-#+end_src
-
-*** Instruction list step
-:PROPERTIES:
-:CUSTOM_ID: step_instr_list
-:END:
-
-The ~step_instr_list~ definition describes the execution of a list of instructions in one big step,
-inductively traversing the list of instructions and applying the ~step_instr~ ([[#step_instr][step_instr]]).
-
-#+name: rtlblock-step_instr_list
-#+begin_src coq
- Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
- | exec_RBcons:
- forall state i state' state'' instrs sp,
- step_instr ge sp state i state' ->
- step_instr_list sp state' instrs state'' ->
- step_instr_list sp state (i :: instrs) state''
- | exec_RBnil:
- forall state sp,
- step_instr_list sp state nil state.
-#+end_src
-
-*** Top-level step
-:PROPERTIES:
-:CUSTOM_ID: rtlblock-step
-:END:
-
-The step function itself then uses this big step of the list of instructions to then show a
-transition from basic block to basic block.
-
-#+name: rtlblock-step
-#+begin_src coq
- Variant step: state -> trace -> state -> Prop :=
- | exec_bblock:
- forall s f sp pc rs rs' m m' t s' bb pr pr',
- f.(fn_code)!pc = Some bb ->
- 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) ->
- step (Callstate s (Internal f) args m)
- E0 (State s f
- (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',
- external_call ef ge args m t res m' ->
- step (Callstate s (External ef) args m)
- t (Returnstate s res m')
- | exec_return:
- 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_src
-
-#+name: rtlblock-rest
-#+begin_src coq
-End RELSEM.
-
-Inductive initial_state (p: program): state -> Prop :=
-| initial_state_intro: forall b f m0,
- let ge := Genv.globalenv p in
- Genv.init_mem p = Some m0 ->
- Genv.find_symbol ge p.(prog_main) = Some b ->
- Genv.find_funct_ptr ge b = Some f ->
- funsig f = signature_main ->
- initial_state p (Callstate nil f nil m0).
-
-Inductive final_state: state -> int -> Prop :=
-| final_state_intro: forall r m,
- final_state (Returnstate nil (Vint r) m) r.
-
-Definition semantics (p: program) :=
- Semantics step (initial_state p) final_state (Genv.globalenv p).
-#+end_src
-
-* RTLPar
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLPar.v
-:END:
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: rtlpar-main
-#+begin_src coq
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Events.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Smallstep.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Coqlib.
-Require Import compcert.lib.Integers.
-Require Import compcert.lib.Maps.
-Require Import compcert.verilog.Op.
-
-Require Import vericert.hls.RTLBlockInstr.
-
-Definition bb := list (list (list instr)).
-
-Definition bblock := @bblock bb.
-Definition code := @code bb.
-Definition function := @function bb.
-Definition fundef := @fundef bb.
-Definition program := @program bb.
-Definition funsig := @funsig bb.
-Definition stackframe := @stackframe bb.
-Definition state := @state bb.
-Definition genv := @genv bb.
-
-Section RELSEM.
-
- Context (ge: genv).
-
- Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
- | exec_RBcons:
- forall state i state' state'' instrs sp,
- step_instr ge sp state i state' ->
- step_instr_list sp state' instrs state'' ->
- step_instr_list sp state (i :: instrs) state''
- | exec_RBnil:
- forall state sp,
- step_instr_list sp state nil state.
-
- Inductive step_instr_seq (sp : val)
- : instr_state -> list (list instr) -> instr_state -> Prop :=
- | exec_instr_seq_cons:
- forall state i state' state'' instrs,
- step_instr_list sp state i state' ->
- step_instr_seq sp state' instrs state'' ->
- step_instr_seq sp state (i :: instrs) state''
- | exec_instr_seq_nil:
- forall state,
- step_instr_seq sp state nil state.
-
- Inductive step_instr_block (sp : val)
- : instr_state -> bb -> instr_state -> Prop :=
- | exec_instr_block_cons:
- forall state i state' state'' instrs,
- step_instr_seq sp state i state' ->
- step_instr_block sp state' instrs state'' ->
- step_instr_block sp state (i :: instrs) state''
- | exec_instr_block_nil:
- forall state,
- step_instr_block sp state nil state.
-
- Inductive step: state -> trace -> state -> Prop :=
- | exec_bblock:
- forall s f sp pc rs rs' m m' t s' bb pr pr',
- f.(fn_code)!pc = Some bb ->
- 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) ->
- step (Callstate s (Internal f) args m)
- E0 (State s
- f
- (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',
- external_call ef ge args m t res m' ->
- step (Callstate s (External ef) args m)
- t (Returnstate s res m')
- | exec_return:
- 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.
-
-Inductive initial_state (p: program): state -> Prop :=
- | initial_state_intro: forall b f m0,
- let ge := Genv.globalenv p in
- Genv.init_mem p = Some m0 ->
- Genv.find_symbol ge p.(prog_main) = Some b ->
- Genv.find_funct_ptr ge b = Some f ->
- funsig f = signature_main ->
- initial_state p (Callstate nil f nil m0).
-
-Inductive final_state: state -> int -> Prop :=
- | final_state_intro: forall r m,
- final_state (Returnstate nil (Vint r) m) r.
-
-Definition semantics (p: program) :=
- Semantics step (initial_state p) final_state (Genv.globalenv p).
-
-Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
- let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
- max_reg_cfi max_body bb.(bb_exit).
-
-Definition max_reg_function (f: function) :=
- Pos.max
- (PTree.fold max_reg_bblock f.(fn_code) 1%positive)
- (fold_left Pos.max f.(fn_params) 1%positive).
-
-Definition max_pc_function (f: function) : positive :=
- PTree.fold (fun m pc i => (Pos.max m
- (pc + match Zlength i.(bb_body)
- with Z.pos p => p | _ => 1 end))%positive)
- f.(fn_code) 1%positive.
-#+end_src
-
-* License
-
-#+name: license
-#+begin_src coq :tangle no
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2022 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/>.
- *)
-#+end_src
diff --git a/docs/scheduler.org b/docs/scheduler.org
deleted file mode 100644
index c8b00ff..0000000
--- a/docs/scheduler.org
+++ /dev/null
@@ -1,2317 +0,0 @@
-#+title: Basic Block Generation
-#+author: Yann Herklotz
-#+email: yann [at] yannherklotz [dot] com
-
-* Scheduler
-:PROPERTIES:
-:header-args:ocaml: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/Schedule.ml
-:END:
-
-#+begin_src ocaml :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: scheduler-main
-#+begin_src ocaml
-open Printf
-open Clflags
-open Camlcoq
-open Datatypes
-open Coqlib
-open Maps
-open AST
-open Kildall
-open Op
-open RTLBlockInstr
-open Predicate
-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
- | RBload _ -> 2
- | 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 (List.nth map i)), 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
- | RBsetpred (_op, _mem, rs, _p) -> acc_dep_instruction_nodst rs
- | 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
- | Plit p'' -> P.to_int p = P.to_int (snd p'')
- | Pand (p1, p2) -> in_predicate p p1 || in_predicate p p2
- | Por (p1, p2) -> in_predicate p p1 || in_predicate p p2
- | Ptrue -> false
- | Pfalse -> false
-
-let get_predicate = function
- | RBop (p, _, _, _) -> p
- | RBload (p, _, _, _, _) -> p
- | RBstore (p, _, _, _, _) -> p
- | RBsetpred (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
- | RBsetpred (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 (Plit (true, 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 (Pand (p, p')) with
- | 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_initial_sv n dfg constr =
- let add_initial_sv' (i, instr) g =
- let pipes = pipeline_stages instr in
- if pipes > 0 then
- List.init pipes (fun i' -> i')
- |> List.fold_left (fun g i' ->
- G.add_edge_e g (encode_var n i i', -1, encode_var n i (i'+1))
- ) g
- else g
- in
- DFG.fold_vertex add_initial_sv' dfg constr
-
-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) (pipeline_stages (snd v1)),
- 0, encode_bb n 1)
- else g')) dfg
-
-let add_data_deps n =
- DFG.fold_edges_e (function ((i1, instr1), _, (i2, _)) -> fun g ->
- let end_sv = pipeline_stages instr1 in
- G.add_edge_e g (encode_var n i1 end_sv, 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 maxf n dfg constr =
- let negated_dfg = negate_graph dfg in
- let max_initial_del = DFG.fold_vertex (fun v1 g ->
- if DFG.in_degree dfg v1 = 0
- then max g (comb_delay (snd v1))
- else g) dfg 0 in
- let longest_path v = BFDFG.all_shortest_paths negated_dfg v
- |> BFDFG.H.to_seq |> List.of_seq
- |> List.map (function (x, y) -> (x, y - max_initial_del)) in
- let constrained_paths = List.filter (function (_, m) -> - m > maxf) 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 maxf))) - 1),
- encode_var n (fst v') 0)
- ) constr (DFG.fold_vertex (fun v l ->
- List.append l (longest_path v (*|> (function l -> List.iter (function (a, x) ->
- printf "c: %d %d\n" (fst a) x) l; l)*) |> constrained_paths (* |> (function l -> List.iter (function (a, x) ->
- printf "%d %d\n" (fst a) x) l; l)*)
- |> 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_initial_sv n dfg
- |> 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, bbtree) s =
- let r = Str.regexp "var\\([0-9]+\\)n\\([0-9]+\\)_0[ ]+\\([0-9]+\\)" in
- let bb = Str.regexp "bb\\([0-9]+\\)_\\([0-9]+\\)[ ]+\\([0-9]+\\)" in
- let upd s = 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 ))
- in
- if Str.string_match r s 0
- then (upd s tree, bbtree)
- else
- (if Str.string_match bb s 0
- then (tree, upd s bbtree)
- else (tree, bbtree))
-
-let solve_constraints constr =
- let (fn, oc) = Filename.open_temp_file "vericert_" "_lp_solve" in
- fprintf oc "%s\n" (print_lp constr);
- close_out oc;
-
- let res = Str.split (Str.regexp_string "\n") (read_process ("lp_solve " ^ fn))
- |> drop 3
- |> List.fold_left parse_soln (IMap.empty, IMap.empty)
- in
- (*Sys.remove fn;*) res
-
-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
-
-let range s e =
- List.init (e - s) (fun i -> i)
- |> List.map (fun x -> x + s)
-
-(** Should generate the [RTLPar] code based on the input [RTLBlock] description. *)
-let transf_rtlpar c c' schedule =
- 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 bb_st_e =
- let m = IMap.find (P.to_int i) (snd schedule) in
- (List.assq 0 m, List.assq 1 m) in
- let i_sched = IMap.find (P.to_int i) (fst 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 body2 = List.fold_left (fun x b ->
- match IMap.find_opt b i_sched_tree with
- | Some i -> i :: x
- | None -> [] :: x
- ) [] (range (fst bb_st_e) (snd bb_st_e + 1))
- |> List.map (List.map (fun x -> (x, List.nth bb_body' x)))
- |> List.rev
- 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))) body2
- (*|> (fun x -> TopoDFG.fold (fun i l -> snd i :: l) x [])
- |> List.rev) body2*)
- 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 = scheduled (*List.fold_left (add_to_tree scheduled) PTree.empty reachable*);
- fn_entrypoint = f.fn_entrypoint
- }
-#+end_src
-
-* RTLPargen
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLPargen.v
-:END:
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: rtlpargen-main
-#+begin_src coq
-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.Predicate.
-Require Import vericert.hls.Abstr.
-Import NE.NonEmptyNotation.
-
-#[local] Open Scope positive.
-#[local] Open Scope forest.
-#[local] Open Scope pred_op.
-#+end_src
-
-** Abstract Computations
-
-Define the abstract computation using the [update] function, which will set each register to its
-symbolic value. First we need to define a few helper functions to correctly translate the
-predicates.
-
-#+name: rtlpargen-generation
-#+begin_src coq
-Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr :=
- match l with
- | 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 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 predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
- NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
- (NE.non_empty_prod p1 p2).
-
-Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B :=
- NE.map (fun x => (fst x, f (snd x))) p.
-
-(*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 => NE.singleton (T, Enil)
- | a :: b => merge' a (merge b)
- 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 :=
- NE.map (fun x => (fst x, (snd x) pa)) pf.
-
-Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C :=
- NE.map (fun x => (fst x, (snd x) pa pb)) pf.
-
-Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D :=
- NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
-
-Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
- match p with
- | Some p' => NE.singleton (p', a)
- | None => NE.singleton (T, a)
- end.
-
-#[local] Open Scope non_empty_scope.
-#[local] Open Scope pred_op.
-
-Fixpoint NEfold_left {A B} (f: A -> B -> A) (l: NE.non_empty B) (a: A) : A :=
- match l with
- | NE.singleton a' => f a a'
- | a' ::| b => NEfold_left f b (f a a')
- end.
-
-Fixpoint NEapp {A} (l m: NE.non_empty A) :=
- match l with
- | NE.singleton a => a ::| m
- | a ::| b => a ::| NEapp b m
- end.
-
-Definition app_predicated' {A: Type} (a b: predicated A) :=
- let negation := ¬ (NEfold_left (fun a b => a ∨ (fst b)) b ⟂) in
- NEapp (NE.map (fun x => (negation ∧ fst x, snd x)) a) b.
-
-Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) :=
- match p with
- | Some p' => NEapp (NE.map (fun x => (¬ p' ∧ fst x, snd x)) a)
- (NE.map (fun x => (p' ∧ fst x, snd x)) b)
- | None => b
- end.
-
-Definition pred_ret {A: Type} (a: A) : predicated A :=
- NE.singleton (T, a).
-
-#+end_src
-
-*** Update Function
-:PROPERTIES:
-:CUSTOM_ID: update-function
-:END:
-
-The [update] function will generate a new forest given an existing forest and a new instruction, so
-that it can evaluate a symbolic expression by folding over a list of instructions. The main problem
-is that predicates need to be merged as well, so that:
-
-1. The predicates are *independent*.
-2. The expression assigned to the register should still be correct.
-
-This is done by multiplying the predicates together, and assigning the negation of the expression to
-the other predicates.
-
-#+name: rtlpargen-update-function
-#+begin_src coq
-Definition update (f : forest) (i : instr) : forest :=
- match i with
- | RBnop => f
- | RBop p op rl r =>
- f # (Reg r) <-
- (app_predicated p
- (f # (Reg r))
- (map_predicated (pred_ret (Eop op)) (merge (list_translation rl f))))
- | RBload p chunk addr rl r =>
- f # (Reg r) <-
- (app_predicated p
- (f # (Reg r))
- (map_predicated
- (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f)))
- (f # Mem)))
- | RBstore p chunk addr rl r =>
- f # Mem <-
- (app_predicated p
- (f # Mem)
- (map_predicated
- (map_predicated
- (predicated_apply2 (map_predicated (pred_ret Estore) (f # (Reg r))) chunk addr)
- (merge (list_translation rl f))) (f # Mem)))
- | RBsetpred p' c args p =>
- f # (Pred p) <-
- (app_predicated p'
- (f # (Pred p))
- (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f))))
- end.
-#+end_src
-
-Implementing which are necessary to show the correctness of the translation validation by
-showing that there aren't any more effects in the resultant RTLPar code than in the RTLBlock code.
-
-Get a sequence from the basic block.
-
-#+name: rtlpargen-abstract-seq
-#+begin_src coq
-Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
- match b with
- | nil => f
- | i :: l => abstract_sequence (update f i) l
- end.
-#+end_src
-
-Check equivalence of control flow instructions. As none of the basic blocks should have been
-moved, none of the labels should be different, meaning the control-flow instructions should match
-exactly.
-
-#+name: rtlpargen-check-functions
-#+begin_src coq
-Definition check_control_flow_instr (c1 c2: cf_instr) : bool :=
- if cf_instr_eq c1 c2 then true else false.
-#+end_src
-
-We define the top-level oracle that will check if two basic blocks are equivalent after a
-scheduling transformation.
-
-#+name: rtlpargen-top-check-functions
-#+begin_src coq
-Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
- match bb with
- | nil =>
- match bbt with
- | nil => true
- | _ => false
- end
- | _ => true
- end.
-
-Definition schedule_oracle (bb: RTLBlock.bblock) (bbt: RTLPar.bblock) : bool :=
- check (abstract_sequence empty (bb_body bb))
- (abstract_sequence empty (concat (concat (bb_body bbt)))) &&
- check_control_flow_instr (bb_exit bb) (bb_exit bbt) &&
- empty_trees (bb_body bb) (bb_body bbt).
-
-Definition check_scheduled_trees := beq2 schedule_oracle.
-
-Ltac solve_scheduled_trees_correct :=
- intros; unfold check_scheduled_trees in *;
- match goal with
- | [ H: context[beq2 _ _ _], x: positive |- _ ] =>
- rewrite beq2_correct in H; specialize (H x)
- end; repeat destruct_match; crush.
-
-Lemma check_scheduled_trees_correct:
- forall f1 f2 x y1,
- check_scheduled_trees f1 f2 = true ->
- PTree.get x f1 = Some y1 ->
- exists y2, PTree.get x f2 = Some y2 /\ schedule_oracle y1 y2 = true.
-Proof. solve_scheduled_trees_correct; eexists; crush. Qed.
-
-Lemma check_scheduled_trees_correct2:
- forall f1 f2 x,
- check_scheduled_trees f1 f2 = true ->
- PTree.get x f1 = None ->
- PTree.get x f2 = None.
-Proof. solve_scheduled_trees_correct. Qed.
-
-#+end_src
-
-** Top-level Functions
-
-#+name: rtlpargen-top-level-functions
-#+begin_src coq
-Parameter schedule : RTLBlock.function -> RTLPar.function.
-
-Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :=
- let tfcode := fn_code (schedule f) in
- if check_scheduled_trees f.(fn_code) tfcode then
- Errors.OK (mkfunction f.(fn_sig)
- f.(fn_params)
- f.(fn_stacksize)
- tfcode
- f.(fn_entrypoint))
- else
- Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
-
-Definition transl_fundef := transf_partial_fundef transl_function.
-
-Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
- transform_partial_program transl_fundef p.
-#+end_src
-
-* RTLPargenproof
-:PROPERTIES:
-:header-args:coq: :comments noweb :noweb no-export :padline yes :tangle ../src/hls/RTLPargenproof.v
-:END:
-
-#+begin_src coq :comments no :padline no :exports none
-<<license>>
-#+end_src
-
-#+name: rtlpargenproof-imports
-#+begin_src coq
-Require Import compcert.backend.Registers.
-Require Import compcert.common.AST.
-Require Import compcert.common.Errors.
-Require Import compcert.common.Linking.
-Require Import compcert.common.Globalenvs.
-Require Import compcert.common.Memory.
-Require Import compcert.common.Values.
-Require Import compcert.lib.Maps.
-
-Require Import vericert.common.Vericertlib.
-Require Import vericert.hls.RTLBlock.
-Require Import vericert.hls.RTLPar.
-Require Import vericert.hls.RTLBlockInstr.
-Require Import vericert.hls.RTLPargen.
-Require Import vericert.hls.Predicate.
-Require Import vericert.hls.Abstr.
-
-#[local] Open Scope positive.
-#[local] Open Scope forest.
-#[local] Open Scope pred_op.
-#+end_src
-
-** RTLBlock to abstract translation
-
-Correctness of translation from RTLBlock to the abstract interpretation language.
-
-#+name: rtlpargenproof-main
-#+begin_src coq
-(*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).
-
-Ltac inv_simp :=
- repeat match goal with
- | H: exists _, _ |- _ => inv H
- end; simplify.
-
-*)
-
-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_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_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_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_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_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. simplify. econstructor. simplify. right. eassumption.
- 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; simplify.
- apply in_app_or in H. inv H. left.
- apply check_dest_l_ex2. exists x0. auto.
- inv H0; auto.
-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 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 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 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 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 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 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 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_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.*)
-*)
-
-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 abstract_interp_empty3 :
- forall A ctx st',
- @sem A ctx empty st' -> match_states (ctx_is ctx) st'.
-Proof.
- inversion 1; subst; simplify. destruct ctx.
- destruct ctx_is.
- constructor; intros.
- - inv H0. specialize (H3 x). inv H3. inv H8. reflexivity.
- - inv H1. specialize (H3 x). inv H3. inv H8. reflexivity.
- - inv H2. inv H8. reflexivity.
-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;
- try solve [repeat econstructor; try erewrite match_states_list;
- try apply PTree_matches; eauto;
- match goal with
- H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
- end].
- - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
- repeat econstructor; try erewrite match_states_list; eauto.
- erewrite <- eval_predf_pr_equiv; eassumption.
- apply PTree_matches; assumption.
- repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
- erewrite <- eval_predf_pr_equiv; eassumption.
- econstructor; auto.
- match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
- repeat econstructor; try erewrite match_states_list; eauto.
- - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
- repeat econstructor; try erewrite match_states_list; eauto.
- erewrite <- eval_predf_pr_equiv; eassumption.
- apply PTree_matches; assumption.
- repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
- erewrite <- eval_predf_pr_equiv; eassumption.
- econstructor; auto.
- match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
- repeat econstructor; try erewrite match_states_list; eauto.
- - destruct p. match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
- repeat econstructor; try erewrite match_states_list; eauto.
- match goal with
- H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
- end.
- erewrite <- eval_predf_pr_equiv; eassumption.
- repeat (econstructor; try apply eval_pred_false); eauto. try erewrite match_states_list; eauto.
- match goal with
- H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
- end.
- erewrite <- eval_predf_pr_equiv; eassumption.
- match goal with H: eval_pred _ _ _ _ |- _ => inv H end.
- repeat econstructor; try erewrite match_states_list; eauto.
- match goal with
- H: forall _, _ |- context[Mem.storev] => erewrite <- H; eauto
- end.
- - admit. Admitted.
-
-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; []; simplify;
- exploit IHa; eauto; []; simplify); 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; []; simplify;
- exploit IHa; eauto; []; simplify); 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; []; simplify;
- exploit IHbb; eauto; []; simplify); repeat econstructor; eauto.
-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. simplify.
- econstructor. split.
- econstructor; eauto. eauto.
-Qed.
-
-Lemma abstract_interp_empty A st : @sem A st empty (ctx_is st).
-Proof. destruct st, ctx_is. simpl. repeat econstructor. 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 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 sem_separate :
- forall A ctx b a st',
- sem ctx (abstract_sequence empty (a ++ b)) st' ->
- exists st'',
- @sem A ctx (abstract_sequence empty a) st''
- /\ @sem A (mk_ctx st'' (ctx_sp ctx) (ctx_ge ctx)) (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; simplify.
- exploit IHb; eauto; inv_simp.
- econstructor; split; eauto.
- rewrite abstract_seq.
- eapply sem_update2; eauto.
- }
-Qed.*)
-
-Lemma sem_update_RBnop :
- forall A ctx f st',
- @sem A ctx f st' -> sem ctx (update f RBnop) st'.
-Proof. auto. Qed.
-
-Lemma sem_update_Op :
- forall A ge sp ist f st' r l o0 o m rs v ps,
- @sem A (mk_ctx ist sp ge) f st' ->
- eval_predf ps o = true ->
- Op.eval_operation ge sp o0 (rs ## l) m = Some v ->
- match_states st' (mk_instr_state rs ps m) ->
- exists tst,
- sem (mk_ctx ist sp ge) (update f (RBop (Some o) o0 l r)) tst
- /\ match_states (mk_instr_state (Regmap.set r v rs) ps m) tst.
-Proof.
- intros. inv H1. inv H. inv H1. inv H3. simplify.
- econstructor. simplify.
- { constructor; try constructor; intros; try solve [rewrite genmap1; now eauto].
- destruct (Pos.eq_dec x r); subst.
- { rewrite map2. specialize (H1 r). inv H1.
-(*}
- }
- 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.*) Admitted.
-
-Lemma sem_update :
- forall A ge sp st x st' st'' st''' f,
- sem (mk_ctx st sp ge) f st' ->
- match_states st' st''' ->
- @step_instr A ge sp st''' x st'' ->
- exists tst, sem (mk_ctx st sp ge) (update f x) tst /\ match_states st'' tst.
-Proof.
- intros. destruct x.
- - inv H1. econstructor. simplify. eauto. symmetry; auto.
- - inv H1. inv H0. econstructor.
- Admitted.
-
-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 (mk_ctx tst sp ge) (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. simplify.
- rewrite abstract_seq.
- exploit IHbb; try eassumption; []; simplify.
- exploit sem_update. apply H1. symmetry; eassumption.
- eauto. simplify. econstructor. split. apply H3.
- auto. }
-Qed.
-
-Lemma abstract_execution_correct:
- forall bb bb' cfi 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 st tst ->
- exists tst', RTLPar.step_instr_block tge sp tst bb' tst'
- /\ match_states st' tst'.
-Proof.
- intros.
- unfold schedule_oracle in *. simplify. unfold empty_trees in H4.
- exploit rtlblock_trans_correct; try eassumption; []; simplify.
-(*) 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.*)Admitted.
-
-Definition match_prog (prog : RTLBlock.program) (tprog : RTLPar.program) :=
- match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq prog tprog.
-
-Inductive match_stackframes: RTLBlock.stackframe -> RTLPar.stackframe -> Prop :=
-| match_stackframe:
- forall f tf res sp pc rs rs' ps ps',
- transl_function f = OK tf ->
- (forall x, rs !! x = rs' !! x) ->
- (forall x, ps !! x = ps' !! x) ->
- match_stackframes (Stackframe res f sp pc rs ps)
- (Stackframe res tf sp pc rs' ps').
-
-Inductive match_states: RTLBlock.state -> RTLPar.state -> Prop :=
-| match_state:
- forall sf f sp pc rs rs' m sf' tf ps ps'
- (TRANSL: transl_function f = OK tf)
- (STACKS: list_forall2 match_stackframes sf sf')
- (REG: forall x, rs !! x = rs' !! x)
- (REG: forall x, ps !! x = ps' !! x),
- match_states (State sf f sp pc rs ps m)
- (State sf' tf sp pc rs' ps' m)
-| match_returnstate:
- forall stack stack' v m
- (STACKS: list_forall2 match_stackframes stack stack'),
- match_states (Returnstate stack v m)
- (Returnstate stack' v m)
-| match_callstate:
- forall stack stack' f tf args m
- (TRANSL: transl_fundef f = OK tf)
- (STACKS: list_forall2 match_stackframes stack stack'),
- match_states (Callstate stack f args m)
- (Callstate stack' tf args m).
-
-Section CORRECTNESS.
-
- Context (prog: RTLBlock.program) (tprog : RTLPar.program).
- Context (TRANSL: match_prog prog tprog).
-
- Let ge : RTLBlock.genv := Globalenvs.Genv.globalenv prog.
- Let tge : RTLPar.genv := Globalenvs.Genv.globalenv tprog.
-
- 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 : rtlgp.
-
- Lemma function_ptr_translated:
- forall (b: Values.block) (f: RTLBlock.fundef),
- Genv.find_funct_ptr ge b = Some f ->
- exists tf,
- Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Errors.OK tf.
- Proof using TRANSL.
- intros. exploit (Genv.find_funct_ptr_match TRANSL); eauto.
- intros (cu & tf & P & Q & R); exists tf; auto.
- Qed.
-
- Lemma functions_translated:
- forall (v: Values.val) (f: RTLBlock.fundef),
- Genv.find_funct ge v = Some f ->
- exists tf,
- Genv.find_funct tge v = Some tf /\ transl_fundef f = Errors.OK tf.
- Proof using TRANSL.
- intros. exploit (Genv.find_funct_match TRANSL); eauto.
- intros (cu & tf & P & Q & R); exists tf; auto.
- Qed.
-
- Lemma senv_preserved:
- Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
- Proof (Genv.senv_transf_partial TRANSL).
- Hint Resolve senv_preserved : rtlgp.
-
- Lemma sig_transl_function:
- forall (f: RTLBlock.fundef) (tf: RTLPar.fundef),
- transl_fundef f = OK tf ->
- funsig tf = funsig f.
- Proof using .
- unfold transl_fundef, transf_partial_fundef, transl_function; intros;
- repeat destruct_match; crush;
- match goal with H: OK _ = OK _ |- _ => inv H end; auto.
- Qed.
- Hint Resolve sig_transl_function : rtlgp.
-
- Hint Resolve Val.lessdef_same : rtlgp.
- Hint Resolve regs_lessdef_regs : rtlgp.
-
- Lemma find_function_translated:
- forall ros rs rs' f,
- (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.
- Proof using TRANSL.
- Ltac ffts := match goal with
- | [ H: forall _, Val.lessdef _ _, r: Registers.reg |- _ ] =>
- specialize (H r); inv H
- | [ H: Vundef = ?r, H1: Genv.find_funct _ ?r = Some _ |- _ ] =>
- rewrite <- H in H1
- | [ H: Genv.find_funct _ Vundef = Some _ |- _] => solve [inv H]
- | _ => solve [exploit functions_translated; eauto]
- end.
- destruct ros; simplify; try rewrite <- H;
- [| rewrite symbols_preserved; destruct_match;
- try (apply function_ptr_translated); crush ];
- intros;
- repeat ffts.
- Qed.
-
- Lemma schedule_oracle_nil:
- forall bb cfi,
- schedule_oracle {| bb_body := nil; bb_exit := cfi |} bb = true ->
- bb_body bb = nil /\ bb_exit bb = cfi.
- Proof using .
- unfold schedule_oracle, check_control_flow_instr.
- simplify; repeat destruct_match; crush.
- Qed.
-
- Lemma schedule_oracle_nil2:
- forall cfi,
- schedule_oracle {| bb_body := nil; bb_exit := cfi |}
- {| bb_body := nil; bb_exit := cfi |} = true.
- Proof using .
- unfold schedule_oracle, check_control_flow_instr.
- simplify; repeat destruct_match; crush.
- Qed.
-
- Lemma eval_op_eq:
- 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;
- [| destruct a; unfold Genv.symbol_address ];
- try rewrite symbols_preserved; auto.
- Qed.
- Hint Resolve eval_op_eq : rtlgp.
-
- Lemma eval_addressing_eq:
- forall sp addr vl,
- Op.eval_addressing ge sp addr vl = Op.eval_addressing tge sp addr vl.
- Proof using TRANSL.
- intros.
- destruct addr;
- unfold Op.eval_addressing, Op.eval_addressing32;
- unfold Genv.symbol_address;
- try rewrite symbols_preserved; auto.
- Qed.
- Hint Resolve eval_addressing_eq : rtlgp.
-
- Lemma ge_preserved_lem:
- ge_preserved ge tge.
- Proof using TRANSL.
- unfold ge_preserved.
- eauto with rtlgp.
- Qed.
- Hint Resolve ge_preserved_lem : rtlgp.
-
- Lemma lessdef_regmap_optget:
- forall or rs rs',
- regs_lessdef rs rs' ->
- Val.lessdef (regmap_optget or Vundef rs) (regmap_optget or Vundef rs').
- 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' ->
- (forall arg v,
- rs !! arg = Vint v ->
- rs' !! arg = Vint v).
- Proof using. intros ? ? H; intros; specialize (H arg); inv H; crush. Qed.
- Hint Resolve int_lessdef : rtlgp.
-
- Ltac semantics_simpl :=
- match goal with
- | [ H: match_states _ _ |- _ ] =>
- let H2 := fresh "H" in
- learn H as H2; inv H2
- | [ H: transl_function ?f = OK _ |- _ ] =>
- let H2 := fresh "TRANSL" in
- learn H as H2;
- unfold transl_function in H2;
- destruct (check_scheduled_trees
- (@fn_code RTLBlock.bb f)
- (@fn_code RTLPar.bb (schedule f))) eqn:?;
- [| discriminate ]; inv H2
- | [ H: context[check_scheduled_trees] |- _ ] =>
- let H2 := fresh "CHECK" in
- learn H as H2;
- eapply check_scheduled_trees_correct in H2; [| solve [eauto] ]
- | [ H: schedule_oracle {| bb_body := nil; bb_exit := _ |} ?bb = true |- _ ] =>
- let H2 := fresh "SCHED" in
- learn H as H2;
- apply schedule_oracle_nil in H2
- | [ 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' |- _ ] =>
- let H3 := fresh "H" in
- learn H; exploit Events.eval_builtin_args_lessdef; [apply H2 | | |];
- eauto with rtlgp; intro H3; learn H3
- | [ H: Events.external_call _ _ _ _ _ _ _ |- _ ] =>
- let H2 := fresh "H" in
- learn H; exploit Events.external_call_mem_extends;
- eauto; intro H2; learn H2
- | [ H: exists _, _ |- _ ] => inv H
- | _ => progress simplify
- end.
-
- Hint Resolve Events.eval_builtin_args_preserved : rtlgp.
- Hint Resolve Events.external_call_symbols_preserved : rtlgp.
- Hint Resolve set_res_lessdef : rtlgp.
- 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' ->
- forall r,
- match_states s r ->
- exists r', step_cf_instr tge r cfi t r' /\ match_states s' r'.
- Proof using TRANSL.
- induction 1; repeat semantics_simpl;
- 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.
- }
- { exploit IHstep_cf_instr; eauto. simplify.
- repeat (try erewrite match_states_list; eauto; econstructor; eauto with rtlgp).
- erewrite eval_predf_pr_equiv; eauto.
- }
- Qed.
-
- Theorem transl_step_correct :
- forall (S1 : RTLBlock.state) t S2,
- RTLBlock.step ge S1 t S2 ->
- forall (R1 : RTLPar.state),
- match_states S1 R1 ->
- exists R2, Smallstep.plus RTLPar.step tge R1 t R2 /\ match_states S2 R2.
- Proof.
-
- induction 1; repeat semantics_simpl.
-
- { 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.
- simplify. destruct x. inv H7.
-
- exploit step_cf_instr_correct; try eassumption. econstructor; eauto.
- simplify.
-
- 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. }
- { 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.
- 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.
-#+end_src
-
-* License
-
-#+name: license
-#+begin_src coq :tangle no
-(*
- * Vericert: Verified high-level synthesis.
- * Copyright (C) 2020-2022 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/>.
- *)
-#+end_src
diff --git a/src/Compiler.v b/src/Compiler.v
index 8882686..cd05aa9 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -16,15 +16,21 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(** * Compiler Proof
+(*|
+==============
+Compiler Proof
+==============
-This is the top-level module of the correctness proof and proves the final backwards simulation
-correct.
+This is the top-level module of the correctness proof and proves the final
+backwards simulation correct.
-** Imports
+Imports
+=======
-We first need to import all of the modules that are used in the correctness proof, which includes
-all of the passes that are performed in Vericert and the CompCert front end. *)
+We first need to import all of the modules that are used in the correctness
+proof, which includes all of the passes that are performed in Vericert and the
+CompCert front end.
+|*)
Require compcert.backend.Selection.
Require compcert.backend.RTL.
@@ -65,10 +71,14 @@ Require vericert.hls.Memorygen.
Require Import vericert.hls.HTLgenproof.
-(** ** Declarations
+(*|
+Declarations
+============
-We then need to declare the external OCaml functions used to print out intermediate steps in the
-compilation, such as [print_RTL], [print_HTL] and [print_RTLBlock]. *)
+We then need to declare the external OCaml functions used to print out
+intermediate steps in the compilation, such as ``print_RTL``, ``print_HTL`` and
+``print_RTLBlock``.
+|*)
Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_HTL: Z -> HTL.program -> unit.
@@ -86,16 +96,20 @@ Proof.
intros; unfold print. destruct (printer prog); auto.
Qed.
-(** We also declare some new notation, which is also used in CompCert to combine the monadic results
-of each pass. *)
+(*|
+We also declare some new notation, which is also used in CompCert to combine the
+monadic results of each pass.
+|*)
Notation "a @@@ b" :=
(Compiler.apply_partial _ _ a b) (at level 50, left associativity).
Notation "a @@ b" :=
(Compiler.apply_total _ _ a b) (at level 50, left associativity).
-(** As printing is used in the translation but does not change the output, we need to prove that it
-has no effect so that it can be removed during the proof. *)
+(*|
+As printing is used in the translation but does not change the output, we need
+to prove that it has no effect so that it can be removed during the proof.
+|*)
Lemma compose_print_identity:
forall (A: Type) (x: res A) (f: A -> unit),
@@ -104,8 +118,10 @@ Proof.
intros. destruct x; simpl. rewrite print_identity. auto. auto.
Qed.
-(** Finally, some optimisation passes are only activated by a flag, which is handled by the following
-functions for partial and total passes. *)
+(*|
+Finally, some optimisation passes are only activated by a flag, which is handled
+by the following functions for partial and total passes.
+|*)
Definition total_if {A: Type}
(flag: unit -> bool) (f: A -> A) (prog: A) : A :=
@@ -156,11 +172,15 @@ Proof.
intros. unfold match_if in *. destruct (flag tt). eauto. subst. apply forward_simulation_identity.
Qed.
-(** *** Top-level Translation
+(*|
+Top-level Translation
+---------------------
-An optimised transformation function from [RTL] to [Verilog] can then be defined, which applies
-the front end compiler optimisations of CompCert to the RTL that is generated and then performs the
-two Vericert passes from RTL to HTL and then from HTL to Verilog. *)
+An optimised transformation function from ``RTL`` to ``Verilog`` can then be
+defined, which applies the front end compiler optimisations of CompCert to the
+RTL that is generated and then performs the two Vericert passes from RTL to HTL
+and then from HTL to Verilog.
+|*)
Definition transf_backend (r : RTL.program) : res Verilog.program :=
OK r
@@ -184,8 +204,10 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
@@ print (print_HTL 1)*)
@@ Veriloggen.transl_program.
-(** The transformation functions from RTL to Verilog are then added to the backend of the CompCert
-transformations from Clight to RTL. *)
+(*|
+The transformation functions from RTL to Verilog are then added to the backend
+of the CompCert transformations from Clight to RTL.
+|*)
Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
OK p
@@ -234,10 +256,13 @@ Definition transf_hls_temp (p : Csyntax.program) : res Verilog.program :=
@@ print (print_HTL 0)
@@ Veriloggen.transl_program.
-(** ** Correctness Proof
+(*|
+Correctness Proof
+=================
-Finally, the top-level definition for all the passes is defined, which combines the [match_prog]
-predicates of each translation pass from C until Verilog. *)
+Finally, the top-level definition for all the passes is defined, which combines
+the ``match_prog`` predicates of each translation pass from C until Verilog.
+|*)
Local Open Scope linking_scope.
@@ -260,14 +285,18 @@ Definition CompCert's_passes :=
::: mkpass Veriloggenproof.match_prog
::: pass_nil _.
-(** These passes are then composed into a larger, top-level [match_prog] predicate which matches a
-C program directly with a Verilog program. *)
+(*|
+These passes are then composed into a larger, top-level ``match_prog`` predicate
+which matches a C program directly with a Verilog program.
+|*)
Definition match_prog: Csyntax.program -> Verilog.program -> Prop :=
pass_match (compose_passes CompCert's_passes).
-(** We then need to prove that this predicate holds, assuming that the translation is performed
-using the [transf_hls] function declared above. *)
+(*|
+We then need to prove that this predicate holds, assuming that the translation
+is performed using the ``transf_hls`` function declared above.
+|*)
Theorem transf_hls_match:
forall p tp,
@@ -369,12 +398,16 @@ Ltac DestructM :=
apply Verilog.semantics_determinate.
Qed.
-(** *** Backward Simulation
+(*|
+Backward Simulation
+-------------------
-The following theorem is a *backward simulation* between the C and Verilog, which proves the
-semantics preservation of the translation. We can assume that the C and Verilog programs match, as
-we have proven previously in [transf_hls_match] that our translation implies that the
-[match_prog] predicate will hold. *)
+The following theorem is a *backward simulation* between the C and Verilog,
+which proves the semantics preservation of the translation. We can assume that
+the C and Verilog programs match, as we have proven previously in
+``transf_hls_match`` that our translation implies that the ``match_prog``
+predicate will hold.
+|*)
Theorem c_semantic_preservation:
forall p tp,
@@ -391,8 +424,11 @@ Proof.
exact (proj2 (cstrategy_semantic_preservation _ _ H)).
Qed.
-(** We can then use [transf_hls_match] to prove the backward simulation where the assumption is
-that the translation is performed using the [transf_hls] function and that it succeeds. *)
+(*|
+We can then use ``transf_hls_match`` to prove the backward simulation where the
+assumption is that the translation is performed using the ``transf_hls``
+function and that it succeeds.
+|*)
Theorem transf_c_program_correct:
forall p tp,
@@ -402,9 +438,12 @@ Proof.
intros. apply c_semantic_preservation. apply transf_hls_match; auto.
Qed.
-(** The final theorem of the semantic preservation of the translation of separate translation units
-can also be proven correct, however, this is only because the translation fails if more than one
-translation unit is passed to Vericert at the moment. *)
+(*|
+The final theorem of the semantic preservation of the translation of separate
+translation units can also be proven correct, however, this is only because the
+translation fails if more than one translation unit is passed to Vericert at the
+moment.
+|*)
Theorem separate_transf_c_program_correct:
forall c_units verilog_units c_program,
diff --git a/src/bourdoncle/Bourdoncle.v b/src/bourdoncle/Bourdoncle.v
index 9d470b7..ef1798a 100644
--- a/src/bourdoncle/Bourdoncle.v
+++ b/src/bourdoncle/Bourdoncle.v
@@ -1,4 +1,6 @@
-(** Type of a Bourdoncle component. *)
+(*|
+Type of a Bourdoncle component.
+|*)
Require Import List.
Require Import BinPos.
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 13ca276..cb9dc2c 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -29,8 +29,9 @@ Import PTree.
Local Open Scope error_monad_scope.
-(** Instance of traverse for [PTree] and [Errors]. This should maybe be generalised
- in the future. *)
+(*|
+Instance of traverse for ``PTree`` and ``Errors``. This should maybe be generalised in the future.
+|*)
Module PTree.
diff --git a/src/hls/Abstr.v b/src/hls/Abstr.v
index 43d7783..9d310fb 100644
--- a/src/hls/Abstr.v
+++ b/src/hls/Abstr.v
@@ -38,11 +38,14 @@ Require Import vericert.hls.Predicate.
#[local] Open Scope positive.
#[local] Open Scope pred_op.
-(** ** Schedule Oracle
+(*|
+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. *)
+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.
@@ -51,8 +54,11 @@ Inductive resource : Set :=
| 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. *)
+(*|
+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.
@@ -174,9 +180,12 @@ Proof.
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. *)
+(*|
+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.
@@ -193,17 +202,21 @@ Module R_indexed.
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.
+(*|
+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. *)
+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 : Type :=
| Ebase : resource -> expression
@@ -312,8 +325,10 @@ Definition predicated A := NE.non_empty (pred_op * A).
Definition pred_expr := predicated expression.
-(** Using IMap we can create a map from resources to any other type, as resources can be uniquely
-identified as positive numbers. *)
+(*|
+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).
@@ -345,8 +360,11 @@ 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. *)
+(*|
+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.
diff --git a/src/hls/Array.v b/src/hls/Array.v
index 0f5ae02..de74611 100644
--- a/src/hls/Array.v
+++ b/src/hls/Array.v
@@ -190,7 +190,10 @@ Proof.
auto using nth_error_nth.
Qed.
-(** Tail recursive version of standard library function. *)
+(*|
+Tail recursive version of standard library function.
+|*)
+
Fixpoint list_repeat' {A : Type} (acc : list A) (a : A) (n : nat) : list A :=
match n with
| O => acc
diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 47f2092..f3af3d8 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -36,10 +36,13 @@ Require Import ValueInt.
Local Open Scope positive.
-(** The purpose of the hardware transfer language (HTL) is to create a more hardware-like layout
-that is still similar to the register transfer language (RTL) that it came from. The main change is
-that function calls become module instantiations and that we now describe a state machine instead of
-a control-flow graph. *)
+(*|
+The purpose of the hardware transfer language (HTL) is to create a more
+hardware-like layout that is still similar to the register transfer language
+(RTL) that it came from. The main change is that function calls become module
+instantiations and that we now describe a state machine instead of a
+control-flow graph.
+|*)
Local Open Scope assocmap.
@@ -84,7 +87,10 @@ Fixpoint init_regs (vl : list value) (rl : list reg) {struct rl} :=
Definition empty_stack (m : module) : Verilog.assocmap_arr :=
(AssocMap.set m.(mod_ram).(ram_mem) (Array.arr_repeat None m.(mod_ram).(ram_size)) (AssocMap.empty Verilog.arr)).
-(** * Operational Semantics *)
+(*|
+Operational Semantics
+=====================
+|*)
Definition genv := Globalenvs.Genv.t fundef unit.
diff --git a/src/hls/HTLPargen.v b/src/hls/HTLPargen.v
index 8c85701..8960ef9 100644
--- a/src/hls/HTLPargen.v
+++ b/src/hls/HTLPargen.v
@@ -405,7 +405,10 @@ Definition translate_eff_addressing (a: Op.addressing) (args: list reg)
| _, _ => error (Errors.msg "HTLPargen: translate_eff_addressing unsuported addressing")
end.
-(** Translate an instruction to a statement. FIX mulhs mulhu *)
+(*|
+Translate an instruction to a statement. FIX mulhs mulhu
+|*)
+
Definition translate_instr (op : Op.operation) (args : list reg) : mon expr :=
match op, args with
| Op.Omove, r::nil => ret (Vvar r)
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index bf4b057..bf1ef1c 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -1004,22 +1004,25 @@ Section CORRECTNESS.
constructor.
Qed.
- (** The proof of semantic preservation for the translation of instructions
- is a simulation argument based on diagrams of the following form:
-<<
- match_states
- code st rs ------------------------- State m st assoc
- || |
- || |
- || |
- \/ v
- code st rs' ------------------------ State m st assoc'
- match_states
->>
- where [tr_code c data control fin rtrn st] is assumed to hold.
-
- The precondition and postcondition is that that should hold is [match_assocmaps rs assoc].
- *)
+(*|
+The proof of semantic preservation for the translation of instructions is a
+simulation argument based on diagrams of the following form:
+
+::
+> match_states
+> code st rs ------------------------- State m st assoc
+> || |
+> || |
+> || |
+> \/ v
+> code st rs' ------------------------ State m st assoc'
+> match_states
+
+where ``tr_code c data control fin rtrn st`` is assumed to hold.
+
+The precondition and postcondition is that that should hold is ``match_assocmaps
+rs assoc``.
+|*)
Definition transl_instr_prop (instr : RTL.instruction) : Prop :=
forall m asr asa fin rtrn st stmt trans res,
@@ -1091,7 +1094,7 @@ Section CORRECTNESS.
apply Smallstep.plus_one.
eapply HTL.step_module; eauto.
inv CONST; assumption.
- inv CONST; assumption.
+ inv CONST; assumption.
(* processing of state *)
econstructor.
crush.
@@ -2569,7 +2572,7 @@ Section CORRECTNESS.
Smallstep.plus HTL.step tge R1 Events.E0 R2 /\ match_states (RTL.State s f sp pc' rs m) R2.
Proof.
intros s f sp pc rs m arg tbl n pc' H H0 H1 R1 MSTATE.
-
+
#[local] Hint Resolve transl_ijumptable_correct : htlproof.*)
Lemma transl_ireturn_correct:
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v
index 265b8f7..165fa91 100644
--- a/src/hls/HTLgenspec.v
+++ b/src/hls/HTLgenspec.v
@@ -120,11 +120,15 @@ Ltac monadInv H :=
((progress simpl in H) || unfold F in H); monadInv1 H
end.
-(** * Relational specification of the translation *)
+(*|
+===========================================
+Relational specification of the translation
+===========================================
-(** We now define inductive predicates that characterise the fact that the
+We now define inductive predicates that characterise the fact that the
statemachine that is created by the translation contains the correct
-translations for each of the elements *)
+translations for each of the elements.
+|*)
Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -> Prop :=
| tr_instr_Inop :
diff --git a/src/hls/IfConversion.v b/src/hls/IfConversion.v
index 1879205..2516109 100644
--- a/src/hls/IfConversion.v
+++ b/src/hls/IfConversion.v
@@ -30,10 +30,14 @@ Require Import vericert.bourdoncle.Bourdoncle.
Parameter build_bourdoncle : function -> (bourdoncle * PMap.t N).
-(** * If-Conversion
-
-This conversion is a verified conversion from RTLBlock back to itself, which performs if-conversion
-on basic blocks to make basic blocks larger. *)
+(*|
+=============
+If-Conversion
+=============
+
+This conversion is a verified conversion from RTLBlock back to itself, which
+performs if-conversion on basic blocks to make basic blocks larger.
+|*)
Definition combine_pred (p: pred_op) (optp: option pred_op) :=
match optp with
diff --git a/src/hls/RICtransf.v b/src/hls/RICtransf.v
index d6e926b..643a3a7 100644
--- a/src/hls/RICtransf.v
+++ b/src/hls/RICtransf.v
@@ -27,12 +27,16 @@ Require Import vericert.hls.RTLBlockInstr.
Require Import vericert.hls.RTLPar.
Require Import vericert.hls.Predicate.
-(** * Reverse If-Conversion
+(*|
+=====================
+Reverse If-Conversion
+=====================
-This transformation takes a scheduling RTLPar block and removes any predicates from it. It can then
-be trivially transformed into linear code again. It works by iteratively selecting a predicate,
-then creating a branch based on it and placing subsequent instructions in one branch or the other.
-*)
+This transformation takes a scheduling RTLPar block and removes any predicates
+from it. It can then be trivially transformed into linear code again. It works
+by iteratively selecting a predicate, then creating a branch based on it and
+placing subsequent instructions in one branch or the other.
+|*)
Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
match l with
diff --git a/src/hls/RTLBlock.v b/src/hls/RTLBlock.v
index 98e032b..ecd7561 100644
--- a/src/hls/RTLBlock.v
+++ b/src/hls/RTLBlock.v
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/scheduler-languages.org::rtlblock-main][rtlblock-main]] *)
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Events.
@@ -31,6 +30,12 @@ Require Import compcert.verilog.Op.
Require Import vericert.hls.RTLBlockInstr.
+(*|
+========
+RTLBlock
+========
+|*)
+
Definition bb := list instr.
Definition bblock := @bblock bb.
@@ -43,16 +48,30 @@ Definition stackframe := @stackframe bb.
Definition state := @state bb.
Definition genv := @genv bb.
-(* rtlblock-main ends here *)
-(* [[file:../../docs/scheduler-languages.org::rtlblock-semantics][rtlblock-semantics]] *)
+(*|
+Semantics
+=========
+
+We first describe the semantics by assuming a global program environment with
+type ~genv~ which was declared earlier.
+|*)
+
Section RELSEM.
Context (ge: genv).
-(* rtlblock-semantics ends here *)
-(* [[file:../../docs/scheduler-languages.org::#step_instr_list][rtlblock-step_instr_list]] *)
- Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
+(*|
+Instruction list step
+---------------------
+
+The ``step_instr_list`` definition describes the execution of a list of
+instructions in one big step, inductively traversing the list of instructions
+and applying the ``step_instr``.
+|*)
+
+ Inductive step_instr_list:
+ val -> instr_state -> list instr -> instr_state -> Prop :=
| exec_RBcons:
forall state i state' state'' instrs sp,
step_instr ge sp state i state' ->
@@ -61,14 +80,21 @@ Section RELSEM.
| exec_RBnil:
forall state sp,
step_instr_list sp state nil state.
-(* rtlblock-step_instr_list ends here *)
-(* [[file:../../docs/scheduler-languages.org::#rtlblock-step][rtlblock-step]] *)
+(*|
+Top-level step
+--------------
+
+The step function itself then uses this big step of the list of instructions to
+then show a transition from basic block to basic block.
+|*)
+
Variant step: state -> trace -> state -> Prop :=
| exec_bblock:
forall s f sp pc rs rs' m m' t s' bb pr pr',
f.(fn_code)!pc = Some bb ->
- step_instr_list sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+ 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:
@@ -90,9 +116,7 @@ Section RELSEM.
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).
-(* rtlblock-step ends here *)
-(* [[file:../../docs/scheduler-languages.org::#rtlblock-step][rtlblock-rest]] *)
End RELSEM.
Inductive initial_state (p: program): state -> Prop :=
@@ -110,4 +134,3 @@ Inductive final_state: state -> int -> Prop :=
Definition semantics (p: program) :=
Semantics step (initial_state p) final_state (Genv.globalenv p).
-(* rtlblock-rest ends here *)
diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index bd40516..d23850a 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-imports][rtlblockinstr-imports]] *)
Require Import Coq.micromega.Lia.
Require Import compcert.backend.Registers.
@@ -31,20 +30,47 @@ Require Import compcert.verilog.Op.
Require Import Predicate.
Require Import Vericertlib.
-(* rtlblockinstr-imports ends here *)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-def][rtlblockinstr-instr-def]] *)
Definition node := positive.
+(*|
+=============
+RTLBlockInstr
+=============
+
+These instructions are used for ``RTLBlock`` and ``RTLPar``, so that they have
+consistent instructions, which greatly simplifies the proofs, as they will by
+default have the same instruction syntax and semantics. The only changes are
+therefore at the top-level of the instructions.
+
+Instruction Definition
+======================
+
+First, we define the instructions that can be placed into a basic block, meaning
+they won't branch. The main changes to how instructions are defined in ``RTL``,
+is that these instructions don't have a next node, as they will be in a basic
+block, and they also have an optional predicate (``pred_op``).
+|*)
+
Inductive instr : Type :=
| RBnop : instr
-| RBop : option pred_op -> operation -> list reg -> reg -> instr
-| RBload : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBstore : option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
-| RBsetpred : option pred_op -> condition -> list reg -> predicate -> instr.
-(* rtlblockinstr-instr-def ends here *)
+| RBop :
+ option pred_op -> operation -> list reg -> reg -> instr
+| RBload :
+ option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBstore :
+ option pred_op -> memory_chunk -> addressing -> list reg -> reg -> instr
+| RBsetpred :
+ option pred_op -> condition -> list reg -> predicate -> instr.
+
+(*|
+Control-Flow Instruction Definition
+===================================
+
+These are the instructions that count as control-flow, and will be placed at the
+end of the basic blocks.
+|*)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-cf-instr-def][rtlblockinstr-cf-instr-def]] *)
Inductive cf_instr : Type :=
| RBcall : signature -> reg + ident -> list reg -> reg -> node -> cf_instr
| RBtailcall : signature -> reg + ident -> list reg -> cf_instr
@@ -55,9 +81,12 @@ Inductive cf_instr : Type :=
| RBreturn : option reg -> cf_instr
| RBgoto : node -> cf_instr
| RBpred_cf : pred_op -> cf_instr -> cf_instr -> cf_instr.
-(* rtlblockinstr-cf-instr-def ends here *)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-helpers][rtlblockinstr-helpers]] *)
+(*|
+Helper Functions
+================
+|*)
+
Fixpoint successors_instr (i : cf_instr) : list node :=
match i with
| RBcall sig ros args res s => s :: nil
@@ -67,7 +96,8 @@ Fixpoint successors_instr (i : cf_instr) : list node :=
| RBjumptable arg tbl => tbl
| RBreturn optarg => nil
| RBgoto n => n :: nil
- | RBpred_cf p c1 c2 => concat (successors_instr c1 :: successors_instr c2 :: nil)
+ | RBpred_cf p c1 c2 =>
+ concat (successors_instr c1 :: successors_instr c2 :: nil)
end.
Definition max_reg_instr (m: positive) (i: instr) :=
@@ -136,7 +166,8 @@ Lemma eval_predf_pr_equiv :
eval_predf ps p = eval_predf ps' p.
Proof.
induction p; simplify; auto;
- try (unfold eval_predf; simplify; repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
+ try (unfold eval_predf; simplify;
+ repeat (destruct_match; []); inv Heqp0; rewrite <- H; auto);
[repeat rewrite eval_predf_Pand|repeat rewrite eval_predf_Por];
erewrite IHp1; try eassumption; erewrite IHp2; eauto.
Qed.
@@ -146,17 +177,30 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
| r1 :: rs, v1 :: vs => Regmap.set r1 v1 (init_regs vs rs)
| _, _ => Regmap.init Vundef
end.
-(* rtlblockinstr-helpers ends here *)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-instr-state][rtlblockinstr-instr-state]] *)
+(*|
+Instruction State
+-----------------
+
+Definition of the instruction state, which contains the following:
+
+:is_rs: This is the current state of the registers.
+:is_ps: This is the current state of the predicate registers, which is in a
+ separate namespace and area compared to the standard registers in [is_rs].
+:is_mem: The current state of the memory.
+|*)
+
Record instr_state := mk_instr_state {
is_rs: regset;
is_ps: predset;
is_mem: mem;
}.
-(* rtlblockinstr-instr-state ends here *)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-type-def][rtlblockinstr-type-def]] *)
+(*|
+Top-Level Type Definitions
+==========================
+|*)
+
Section DEFINITION.
Context {bblock_body: Type}.
@@ -193,11 +237,17 @@ Section DEFINITION.
(sp: val) (**r stack pointer in calling function *)
(pc: node) (**r program point in calling function *)
(rs: regset) (**r register state in calling function *)
- (pr: predset), (**r predicate state of the calling function *)
+ (pr: predset), (**r predicate state of the calling
+ function *)
stackframe.
-(* rtlblockinstr-type-def ends here *)
-(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *)
+(*|
+State Definition
+----------------
+
+Definition of the ``state`` type, which is used by the ``step`` functions.
+|*)
+
Variant state : Type :=
| State:
forall (stack: list stackframe) (**r call stack *)
@@ -219,13 +269,14 @@ Section DEFINITION.
(v: val) (**r return value for the call *)
(m: mem), (**r memory state *)
state.
-(* rtlblockinstr-state ends here *)
-(* [[file:../../docs/scheduler-languages.org::#state][rtlblockinstr-state]] *)
End DEFINITION.
-(* rtlblockinstr-state ends here *)
-(* [[file:../../docs/scheduler-languages.org::rtlblockinstr-semantics][rtlblockinstr-semantics]] *)
+(*|
+Semantics
+=========
+|*)
+
Section RELSEM.
Context {bblock_body : Type}.
@@ -245,7 +296,8 @@ Section RELSEM.
end
end.
- Inductive eval_pred: option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
+ Inductive eval_pred:
+ option pred_op -> instr_state -> instr_state -> instr_state -> Prop :=
| eval_pred_true:
forall i i' p,
eval_predf (is_ps i) p = true ->
@@ -256,9 +308,7 @@ Section RELSEM.
eval_pred (Some p) i i' i
| eval_pred_none:
forall i i', eval_pred None i i' i.
-(* rtlblockinstr-semantics ends here *)
-(* [[file:../../docs/scheduler-languages.org::#step_instr][rtlblockinstr-step_instr]] *)
Inductive step_instr: val -> instr_state -> instr -> instr_state -> Prop :=
| exec_RBnop:
forall sp ist,
@@ -266,28 +316,33 @@ Section RELSEM.
| exec_RBop:
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 ->
+ 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 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
+ 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 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
+ 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 p' ist,
Op.eval_condition c rs##args m = Some b ->
- eval_pred p' (mk_instr_state rs pr m) (mk_instr_state rs (pr#p <- b) m) ist ->
- step_instr sp (mk_instr_state rs pr m) (RBsetpred p' c args p) ist.
-(* rtlblockinstr-step_instr ends here *)
+ eval_pred p' (mk_instr_state rs pr m)
+ (mk_instr_state rs (pr#p <- b) m) ist ->
+ step_instr sp (mk_instr_state rs pr m)
+ (RBsetpred p' c args p) ist.
-(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-step_cf_instr]] *)
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' pr,
@@ -300,7 +355,8 @@ Section RELSEM.
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 pr 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 pr,
@@ -327,13 +383,13 @@ Section RELSEM.
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)
+ 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'.
-(* rtlblockinstr-step_cf_instr ends here *)
+ 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'.
-(* [[file:../../docs/scheduler-languages.org::#step_cf_instr][rtlblockinstr-end_RELSEM]] *)
End RELSEM.
-(* rtlblockinstr-end_RELSEM ends here *)
diff --git a/src/hls/RTLBlockgen.v b/src/hls/RTLBlockgen.v
index beca0ea..5d7376d 100644
--- a/src/hls/RTLBlockgen.v
+++ b/src/hls/RTLBlockgen.v
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/basic-block-generation.org::rtlblockgen-imports][rtlblockgen-imports]] *)
Require compcert.backend.RTL.
Require Import compcert.common.AST.
Require Import compcert.lib.Maps.
@@ -28,7 +27,6 @@ Require Import vericert.hls.RTLBlockInstr.
Require Import vericert.hls.RTLBlock.
#[local] Open Scope positive.
-(* rtlblockgen-imports ends here *)
Lemma comparison_eq: forall (x y : comparison), {x = y} + {x <> y}.
Proof.
@@ -148,15 +146,19 @@ Defined.
Definition ceq {A: Type} (eqd: forall a b: A, {a = b} + {a <> b}) (a b: A): bool :=
if eqd a b then true else false.
-(* [[file:../../docs/basic-block-generation.org::rtlblockgen-main][rtlblockgen-main]] *)
Parameter partition : RTL.function -> Errors.res function.
-(** [find_block max nodes index]: Does not need to be sorted, because we use filter and the max fold
- function to find the desired element. *)
+(*|
+``find_block max nodes index``: Does not need to be sorted, because we use
+filter and the max fold function to find the desired element.
+
+ .. coq::
+|*)
+
Definition find_block (max: positive) (nodes: list positive) (index: positive) : positive :=
List.fold_right Pos.min max (List.filter (fun x => (index <=? x)) nodes).
-(*Compute find_block (2::94::28::40::19::nil) 40.*)
+(*Compute find_block 100 (2::94::48::39::19::nil) 40.*)
Definition check_instr (n: positive) (istr: RTL.instruction) (istr': instr) :=
match istr, istr' with
@@ -287,4 +289,3 @@ Definition transl_fundef := transf_partial_fundef transl_function.
Definition transl_program : RTL.program -> Errors.res program :=
transform_partial_program transl_fundef.
-(* rtlblockgen-main ends here *)
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index d51e5d4..4568185 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -16,25 +16,47 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-imports][rtlblockgenproof-imports]] *)
Require compcert.backend.RTL.
Require Import compcert.common.AST.
Require Import compcert.lib.Maps.
+Require Import compcert.common.Errors.
+Require Import vericert.hls.RTLBlockInstr.
Require Import vericert.hls.RTLBlock.
Require Import vericert.hls.RTLBlockgen.
-(* rtlblockgenproof-imports ends here *)
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-match-states][rtlblockgenproof-match-states]] *)
+(*|
+Defining a find block specification
+-----------------------------------
+
+Basically, it should be able to find the location of the block without using the
+``find_block`` function, so that this is more useful for the proofs. There are
+various different types of options that could come up though:
+
+1. The instruction is a standard instruction present inside of a basic block.
+2. The instruction is a standard instruction which ends with a ``goto``.
+3. The instruction is a control-flow instruction.
+
+For case number 1, there should exist a value in the list of instructions, such
+that the instructions match exactly, and the indices match as well. In the
+original code, this instruction must have been going from the current node to
+the node - 1. For case number 2, there should be an instruction at the right
+index again, however, this time there will also be a ``goto`` instruction in the
+control-flow part of the basic block.
+|*)
+
+(*Definition find_block_spec (c1: RTL.code) (c2: code) :=
+ forall x i,
+ c1 ! x = Some i ->
+ exists y li, c2 ! y = Some li /\ nth_error li.(bb_body) ((Pos.to_nat y) - (Pos.to_nat x))%nat = Some i.
+
Inductive match_states : RTL.state -> RTLBlock.state -> Prop :=
| match_state :
forall stk f tf sp pc rs m
(TF: transl_function f = OK tf),
- match_states (RTL.State stk f sp pc rs m)
- (RTLBlock.State stk tf sp (find_block max n i) rs m).
-(* rtlblockgenproof-match-states ends here *)
+ match_states (RTL.State stk f sp pc rs m)
+ (State stk tf sp (find_block max n i) rs m).
-(* [[file:../../docs/basic-block-generation.org::rtlblockgenproof-correctness][rtlblockgenproof-correctness]] *)
Section CORRECTNESS.
Context (prog : RTL.program).
@@ -49,4 +71,4 @@ Section CORRECTNESS.
apply senv_preserved.
End CORRECTNESS.
-(* rtlblockgenproof-correctness ends here *)
+*)
diff --git a/src/hls/RTLPar.v b/src/hls/RTLPar.v
index f380d19..e0f657c 100644
--- a/src/hls/RTLPar.v
+++ b/src/hls/RTLPar.v
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/scheduler-languages.org::rtlpar-main][rtlpar-main]] *)
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Events.
@@ -47,15 +46,16 @@ Section RELSEM.
Context (ge: genv).
- Inductive step_instr_list: val -> instr_state -> list instr -> instr_state -> Prop :=
- | exec_RBcons:
- forall state i state' state'' instrs sp,
- step_instr ge sp state i state' ->
- step_instr_list sp state' instrs state'' ->
- step_instr_list sp state (i :: instrs) state''
- | exec_RBnil:
- forall state sp,
- step_instr_list sp state nil state.
+ Inductive step_instr_list:
+ val -> instr_state -> list instr -> instr_state -> Prop :=
+ | exec_RBcons:
+ forall state i state' state'' instrs sp,
+ step_instr ge sp state i state' ->
+ step_instr_list sp state' instrs state'' ->
+ step_instr_list sp state (i :: instrs) state''
+ | exec_RBnil:
+ forall state sp,
+ step_instr_list sp state nil state.
Inductive step_instr_seq (sp : val)
: instr_state -> list (list instr) -> instr_state -> Prop :=
@@ -83,7 +83,8 @@ Section RELSEM.
| exec_bblock:
forall s f sp pc rs rs' m m' t s' bb pr pr',
f.(fn_code)!pc = Some bb ->
- step_instr_block sp (mk_instr_state rs pr m) bb.(bb_body) (mk_instr_state rs' pr' m') ->
+ 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:
@@ -126,7 +127,11 @@ Definition semantics (p: program) :=
Semantics step (initial_state p) final_state (Genv.globalenv p).
Definition max_reg_bblock (m : positive) (pc : node) (bb : bblock) :=
- let max_body := fold_left (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x) bb.(bb_body) m in
+ let max_body :=
+ fold_left
+ (fun x l => fold_left (fun x' l' => fold_left max_reg_instr l' x') l x)
+ bb.(bb_body) m
+ in
max_reg_cfi max_body bb.(bb_exit).
Definition max_reg_function (f: function) :=
@@ -135,8 +140,9 @@ Definition max_reg_function (f: function) :=
(fold_left Pos.max f.(fn_params) 1%positive).
Definition max_pc_function (f: function) : positive :=
- PTree.fold (fun m pc i => (Pos.max m
- (pc + match Zlength i.(bb_body)
- with Z.pos p => p | _ => 1 end))%positive)
- f.(fn_code) 1%positive.
-(* rtlpar-main ends here *)
+ PTree.fold
+ (fun m pc i =>
+ (Pos.max m
+ (pc + match Zlength i.(bb_body)
+ with Z.pos p => p | _ => 1 end))%positive)
+ f.(fn_code) 1%positive.
diff --git a/src/hls/RTLPargen.v b/src/hls/RTLPargen.v
index 31ea51f..d425049 100644
--- a/src/hls/RTLPargen.v
+++ b/src/hls/RTLPargen.v
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/scheduler.org::rtlpargen-main][rtlpargen-main]] *)
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Globalenvs.
@@ -38,10 +37,22 @@ Import NE.NonEmptyNotation.
#[local] Open Scope positive.
#[local] Open Scope forest.
#[local] Open Scope pred_op.
-(* rtlpargen-main ends here *)
-(* [[file:../../docs/scheduler.org::rtlpargen-generation][rtlpargen-generation]] *)
-Fixpoint list_translation (l : list reg) (f : forest) {struct l} : list pred_expr :=
+(*|
+=========
+RTLPargen
+=========
+
+Abstract Computations
+=====================
+
+Define the abstract computation using the [update] function, which will set each
+register to its symbolic value. First we need to define a few helper functions
+to correctly translate the predicates.
+|*)
+
+Fixpoint list_translation (l : list reg) (f : forest) {struct l}
+ : list pred_expr :=
match l with
| nil => nil
| i :: l => (f # (Reg i)) :: (list_translation l f)
@@ -65,7 +76,8 @@ Definition merge'' x :=
| ((a, e), (b, el)) => (merge''' a b, Econs e el)
end.
-Definition map_pred_op {A B} (pf: option pred_op * (A -> B)) (pa: option pred_op * A): option pred_op * B :=
+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.
@@ -74,8 +86,8 @@ Definition predicated_prod {A B: Type} (p1: predicated A) (p2: predicated B) :=
NE.map (fun x => match x with ((a, b), (c, d)) => (Pand a c, (b, d)) end)
(NE.non_empty_prod p1 p2).
-Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A): predicated B :=
- NE.map (fun x => (fst x, f (snd x))) p.
+Definition predicated_map {A B: Type} (f: A -> B) (p: predicated A)
+ : predicated B := NE.map (fun x => (fst x, f (snd x))) p.
(*map (fun x => (fst x, Econs (snd x) Enil)) pel*)
Definition merge' (pel: pred_expr) (tpel: predicated expression_list) :=
@@ -87,16 +99,20 @@ Fixpoint merge (pel: list pred_expr): predicated expression_list :=
| a :: b => merge' a (merge b)
end.
-Definition map_predicated {A B} (pf: predicated (A -> B)) (pa: predicated A): predicated B :=
+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 :=
+Definition predicated_apply1 {A B} (pf: predicated (A -> B)) (pa: A)
+ : predicated B :=
NE.map (fun x => (fst x, (snd x) pa)) pf.
-Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A) (pb: B): predicated C :=
+Definition predicated_apply2 {A B C} (pf: predicated (A -> B -> C)) (pa: A)
+ (pb: B): predicated C :=
NE.map (fun x => (fst x, (snd x) pa pb)) pf.
-Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D)) (pa: A) (pb: B) (pc: C): predicated D :=
+Definition predicated_apply3 {A B C D} (pf: predicated (A -> B -> C -> D))
+ (pa: A) (pb: B) (pc: C): predicated D :=
NE.map (fun x => (fst x, (snd x) pa pb pc)) pf.
Definition predicated_from_opt {A: Type} (p: option pred_op) (a: A) :=
@@ -133,9 +149,23 @@ Definition app_predicated {A: Type} (p: option pred_op) (a b: predicated A) :=
Definition pred_ret {A: Type} (a: A) : predicated A :=
NE.singleton (T, a).
-(* rtlpargen-generation ends here *)
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-update-function]] *)
+(*|
+Update Function
+---------------
+
+The ``update`` function will generate a new forest given an existing forest and
+a new instruction, so that it can evaluate a symbolic expression by folding over
+a list of instructions. The main problem is that predicates need to be merged
+as well, so that:
+
+1. The predicates are *independent*.
+2. The expression assigned to the register should still be correct.
+
+This is done by multiplying the predicates together, and assigning the negation
+of the expression to the other predicates.
+|*)
+
Definition update (f : forest) (i : instr) : forest :=
match i with
| RBnop => f
@@ -149,7 +179,8 @@ Definition update (f : forest) (i : instr) : forest :=
(app_predicated p
(f # (Reg r))
(map_predicated
- (map_predicated (pred_ret (Eload chunk addr)) (merge (list_translation rl f)))
+ (map_predicated (pred_ret (Eload chunk addr))
+ (merge (list_translation rl f)))
(f # Mem)))
| RBstore p chunk addr rl r =>
f # Mem <-
@@ -157,30 +188,45 @@ Definition update (f : forest) (i : instr) : forest :=
(f # Mem)
(map_predicated
(map_predicated
- (predicated_apply2 (map_predicated (pred_ret Estore) (f # (Reg r))) chunk addr)
+ (predicated_apply2 (map_predicated (pred_ret Estore)
+ (f # (Reg r))) chunk addr)
(merge (list_translation rl f))) (f # Mem)))
| RBsetpred p' c args p =>
f # (Pred p) <-
(app_predicated p'
(f # (Pred p))
- (map_predicated (pred_ret (Esetpred c)) (merge (list_translation args f))))
+ (map_predicated (pred_ret (Esetpred c))
+ (merge (list_translation args f))))
end.
-(* rtlpargen-update-function ends here *)
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-abstract-seq]] *)
+(*|
+Implementing which are necessary to show the correctness of the translation
+validation by showing that there aren't any more effects in the resultant RTLPar
+code than in the RTLBlock code.
+
+Get a sequence from the basic block.
+|*)
+
Fixpoint abstract_sequence (f : forest) (b : list instr) : forest :=
match b with
| nil => f
| i :: l => abstract_sequence (update f i) l
end.
-(* rtlpargen-abstract-seq ends here *)
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-check-functions]] *)
+(*|
+Check equivalence of control flow instructions. As none of the basic blocks
+should have been moved, none of the labels should be different, meaning the
+control-flow instructions should match exactly.
+|*)
+
Definition check_control_flow_instr (c1 c2: cf_instr) : bool :=
if cf_instr_eq c1 c2 then true else false.
-(* rtlpargen-check-functions ends here *)
-(* [[file:../../docs/scheduler.org::#update-function][rtlpargen-top-check-functions]] *)
+(*|
+We define the top-level oracle that will check if two basic blocks are
+equivalent after a scheduling transformation.
+|*)
+
Definition empty_trees (bb: RTLBlock.bb) (bbt: RTLPar.bb) : bool :=
match bb with
| nil =>
@@ -219,12 +265,16 @@ Lemma check_scheduled_trees_correct2:
PTree.get x f1 = None ->
PTree.get x f2 = None.
Proof. solve_scheduled_trees_correct. Qed.
-(* rtlpargen-top-check-functions ends here *)
-(* [[file:../../docs/scheduler.org::rtlpargen-top-level-functions][rtlpargen-top-level-functions]] *)
+(*|
+Top-level Functions
+===================
+|*)
+
Parameter schedule : RTLBlock.function -> RTLPar.function.
-Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :=
+Definition transl_function (f: RTLBlock.function)
+ : Errors.res RTLPar.function :=
let tfcode := fn_code (schedule f) in
if check_scheduled_trees f.(fn_code) tfcode then
Errors.OK (mkfunction f.(fn_sig)
@@ -233,10 +283,10 @@ Definition transl_function (f: RTLBlock.function) : Errors.res RTLPar.function :
tfcode
f.(fn_entrypoint))
else
- Errors.Error (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
+ Errors.Error
+ (Errors.msg "RTLPargen: Could not prove the blocks equivalent.").
Definition transl_fundef := transf_partial_fundef transl_function.
Definition transl_program (p : RTLBlock.program) : Errors.res RTLPar.program :=
transform_partial_program transl_fundef p.
-(* rtlpargen-top-level-functions ends here *)
diff --git a/src/hls/RTLPargenproof.v b/src/hls/RTLPargenproof.v
index 6d61572..4e88b13 100644
--- a/src/hls/RTLPargenproof.v
+++ b/src/hls/RTLPargenproof.v
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/scheduler.org::rtlpargenproof-imports][rtlpargenproof-imports]] *)
Require Import compcert.backend.Registers.
Require Import compcert.common.AST.
Require Import compcert.common.Errors.
@@ -37,9 +36,18 @@ Require Import vericert.hls.Abstr.
#[local] Open Scope positive.
#[local] Open Scope forest.
#[local] Open Scope pred_op.
-(* rtlpargenproof-imports ends here *)
-(* [[file:../../docs/scheduler.org::rtlpargenproof-main][rtlpargenproof-main]] *)
+(*|
+==============
+RTLPargenproof
+==============
+
+RTLBlock to abstract translation
+================================
+
+Correctness of translation from RTLBlock to the abstract interpretation language.
+|*)
+
(*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.
@@ -1134,4 +1142,3 @@ Proof. induction 2; try rewrite H; eauto with barg. Qed.
Qed.
End CORRECTNESS.
-(* rtlpargenproof-main ends here *)
diff --git a/src/hls/Schedule.ml b/src/hls/Schedule.ml
index 3a5351e..70395e7 100644
--- a/src/hls/Schedule.ml
+++ b/src/hls/Schedule.ml
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-(* [[file:../../docs/scheduler.org::scheduler-main][scheduler-main]] *)
open Printf
open Clflags
open Camlcoq
@@ -882,4 +881,3 @@ let schedule_fn (f : RTLBlock.coq_function) : RTLPar.coq_function =
fn_code = scheduled (*List.fold_left (add_to_tree scheduled) PTree.empty reachable*);
fn_entrypoint = f.fn_entrypoint
}
-(* scheduler-main ends here *)
diff --git a/src/hls/ValueInt.v b/src/hls/ValueInt.v
index e434abc..06b5630 100644
--- a/src/hls/ValueInt.v
+++ b/src/hls/ValueInt.v
@@ -22,22 +22,31 @@ From compcert Require Import lib.Integers common.Values.
From vericert Require Import Vericertlib.
(* end hide *)
-(** * Value
+(*|
+=====
+Value
+=====
-A [value] is a bitvector with a specific size. We are using the implementation
+A ``value`` is a bitvector with a specific size. We are using the implementation
of the bitvector by mit-plv/bbv, because it has many theorems that we can reuse.
-However, we need to wrap it with an [Inductive] so that we can specify and match
-on the size of the [value]. This is necessary so that we can easily store
-[value]s of different sizes in a list or in a map.
+However, we need to wrap it with an ``Inductive`` so that we can specify and
+match on the size of the ``value``. This is necessary so that we can easily
+store ``value`` of different sizes in a list or in a map.
-Using the default [word], this would not be possible, as the size is part of the type. *)
+Using the default ``word``, this would not be possible, as the size is part of
+the type.
+|*)
Definition value : Type := int.
-(** ** Value conversions
+(*|
+Value conversions
+=================
-Various conversions to different number types such as [N], [Z], [positive] and
-[int], where the last one is a theory of integers of powers of 2 in CompCert. *)
+Various conversions to different number types such as ``N``, ``Z``, ``positive``
+and ``int``, where the last one is a theory of integers of powers of 2 in
+CompCert.
+|*)
Definition valueToNat (v : value) : nat :=
Z.to_nat (Int.unsigned v).
@@ -83,10 +92,12 @@ Definition valToValue (v : Values.val) : option value :=
| _ => None
end.
-(** Convert a [value] to a [bool], so that choices can be made based on the
-result. This is also because comparison operators will give back [value] instead
-of [bool], so if they are in a condition, they will have to be converted before
-they can be used. *)
+(*|
+Convert a ``value`` to a ``bool``, so that choices can be made based on the
+result. This is also because comparison operators will give back ``value``
+instead of ``bool``, so if they are in a condition, they will have to be
+converted before they can be used.
+|*)
Definition valueToBool (v : value) : bool :=
if Z.eqb (uvalueToZ v) 0 then false else true.
@@ -94,7 +105,10 @@ Definition valueToBool (v : value) : bool :=
Definition boolToValue (b : bool) : value :=
natToValue (if b then 1 else 0).
-(** ** Arithmetic operations *)
+(*|
+Arithmetic operations
+---------------------
+|*)
Inductive val_value_lessdef: val -> value -> Prop :=
| val_value_lessdef_int:
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index 7561f77..72140cd 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -142,23 +142,28 @@ Definition nonblock_reg (r : reg) (asr : reg_associations) (v : value) :=
Inductive scl_decl : Type := VScalar (sz : nat).
Inductive arr_decl : Type := VArray (sz : nat) (ln : nat).
-(** ** Verilog AST
+(*|
+Verilog AST
+===========
The Verilog AST is defined here, which is the target language of the
compilation.
-*** Value
+Value
+-----
-The Verilog [value] is a bitvector containg a size and the actual bitvector. In
-this case, the [Word.word] type is used as many theorems about that bitvector
-have already been proven.
+The Verilog ``value`` is a bitvector containg a size and the actual
+bitvector. In this case, the ``Word.word`` type is used as many theorems about
+that bitvector have already been proven.
-*** Binary Operators
+Binary Operators
+----------------
These are the binary operations that can be represented in Verilog. Ideally,
multiplication and division would be done by custom modules which could al so be
scheduled properly. However, for now every Verilog operator is assumed to take
-one clock cycle. *)
+one clock cycle.
+|*)
Inductive binop : Type :=
| Vadd : binop (** addition (binary [+]) *)
@@ -186,13 +191,19 @@ Inductive binop : Type :=
| Vshru : binop. (** shift right unsigned ([>>]) *)
(* Vror : binop (** shift right unsigned ([>>]) *)*)
-(** *** Unary Operators *)
+(*|
+Unary Operators
+---------------
+|*)
Inductive unop : Type :=
| Vneg (** negation ([-]) *)
| Vnot. (** not operation [!] *)
-(** *** Expressions *)
+(*|
+Expressions
+-----------
+|*)
Inductive expr : Type :=
| Vlit : value -> expr
@@ -207,7 +218,10 @@ Inductive expr : Type :=
Definition posToExpr (p : positive) : expr :=
Vlit (posToValue p).
-(** *** Statements *)
+(*|
+Statements
+----------
+|*)
Inductive stmnt : Type :=
| Vskip : stmnt
@@ -220,13 +234,17 @@ with stmnt_expr_list : Type :=
| Stmntnil : stmnt_expr_list
| Stmntcons : expr -> stmnt -> stmnt_expr_list -> stmnt_expr_list.
-(** *** Edges
+(*|
+Edges
+-----
-These define when an always block should be triggered, for example if the always block should be
-triggered synchronously at the clock edge, or asynchronously for combinational logic.
+These define when an always block should be triggered, for example if the always
+block should be triggered synchronously at the clock edge, or asynchronously for
+combinational logic.
-[edge] is not part of [stmnt] in this formalisation because is closer to the semantics that are
-used. *)
+``edge`` is not part of ``stmnt`` in this formalisation because is closer to the
+semantics that are used.
+|*)
Inductive edge : Type :=
| Vposedge : reg -> edge
@@ -234,11 +252,15 @@ Inductive edge : Type :=
| Valledge : edge
| Voredge : edge -> edge -> edge.
-(** *** Module Items
+(*|
+Module Items
+------------
-Module items can either be declarations ([Vdecl]) or always blocks ([Valways]). The declarations
-are always register declarations as combinational logic can be done using combinational always block
-instead of continuous assignments. *)
+Module items can either be declarations (``Vdecl``) or always blocks
+(``Valways``). The declarations are always register declarations as
+combinational logic can be done using combinational always block instead of
+continuous assignments.
+|*)
Inductive io : Type :=
| Vinput : io
@@ -255,15 +277,17 @@ Inductive module_item : Type :=
| Valways_ff : edge -> stmnt -> module_item
| Valways_comb : edge -> stmnt -> module_item.
-(** The main module type containing all the important control signals
+(*|
+The main module type containing all the important control signals
-- [mod_start] If set, starts the computations in the module.
-- [mod_reset] If set, reset the state in the module.
-- [mod_clk] The clock that controls the computation in the module.
-- [mod_args] The arguments to the module.
-- [mod_finish] Bit that is set if the result is ready.
-- [mod_return] The return value that was computed.
-- [mod_body] The body of the module, including the state machine. *)
+:mod_start: If set, starts the computations in the module.
+:mod_reset: If set, reset the state in the module.
+:mod_clk: The clock that controls the computation in the module.
+:mod_args: The arguments to the module.
+:mod_finish: Bit that is set if the result is ready.
+:mod_return: The return value that was computed.
+:mod_body: The body of the module, including the state machine.
+|*)
Record module : Type := mkmodule {
mod_start : reg;
@@ -271,7 +295,8 @@ Record module : Type := mkmodule {
mod_clk : reg;
mod_finish : reg;
mod_return : reg;
- mod_st : reg; (**r Variable that defines the current state, it should be internal. *)
+ mod_st : reg; (**r Variable that defines the current state,
+ it should be internal. *)
mod_stk : reg;
mod_stk_len : nat;
mod_args : list reg;
@@ -283,33 +308,39 @@ Definition fundef := AST.fundef module.
Definition program := AST.program fundef unit.
-(** Convert a [positive] to an expression directly, setting it to the right size. *)
+(*|
+Convert a ``positive`` to an expression directly, setting it to the right size.
+|*)
+
Definition posToLit (p : positive) : expr :=
Vlit (posToValue p).
Definition fext := unit.
Definition fextclk := nat -> fext.
-(** *** State
+(*|
+State
+-----
-The [state] contains the following items:
+The ``state`` contains the following items:
-- Current [module] that is being worked on, so that the state variable can be
-retrieved and set appropriately.
-- Current [module_item] which is being worked on.
-- A contiunation ([cont]) which defines what to do next. The option is to
- either evaluate another module item or go to the next clock cycle. Finally
- it could also end if the finish flag of the module goes high.
+- Current ``module`` that is being worked on, so that the state variable can be
+ retrieved and set appropriately.
+- Current ``module_item`` which is being worked on.
+- A contiunation (``cont``) which defines what to do next. The option is to
+ either evaluate another module item or go to the next clock cycle. Finally it
+ could also end if the finish flag of the module goes high.
- Association list containing the blocking assignments made, or assignments made
in previous clock cycles.
- Nonblocking association list containing all the nonblocking assignments made
in the current module.
- The environment containing values for the input.
-- The program counter which determines the value for the state in this version of
- Verilog, as the Verilog was generated by the RTL, which means that we have to
- make an assumption about how it looks. In this case, that it contains state
- which determines which part of the Verilog is executed. This is then the part
- of the Verilog that should match with the RTL. *)
+- The program counter which determines the value for the state in this version
+ of Verilog, as the Verilog was generated by the RTL, which means that we have
+ to make an assumption about how it looks. In this case, that it contains
+ state which determines which part of the Verilog is executed. This is then
+ the part of the Verilog that should match with the RTL.
+|*)
Inductive stackframe : Type :=
Stackframe :
@@ -429,7 +460,9 @@ Definition handle_def {A : Type} (a : A) (val : option A)
Local Open Scope error_monad_scope.
-(** Return the location of the lhs of an assignment. *)
+(*|
+Return the location of the lhs of an assignment.
+|*)
Inductive location : Type :=
| LocReg (_ : reg)
generated by cgit (git 2.34.1) at 2024-06-28 23:56:26 +0000