1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
|
(*
* Vericert: Verified high-level synthesis.
* Copyright (C) 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/>.
*)
Require Import compcert.common.AST.
Require Import compcert.common.Errors.
Require Import compcert.common.Globalenvs.
Require Import compcert.lib.Integers.
Require Import compcert.lib.Maps.
Require Import vericert.common.Vericertlib.
Require Import vericert.hls.RTLBlockInstr.
Require Import vericert.hls.RTLPar.
Require Import vericert.hls.Predicate.
(** * 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.
*)
Fixpoint existsb_val {A B} (f: A -> option B) (l : list A) : option B :=
match l with
| nil => None
| a :: l0 =>
match f a, existsb_val f l0 with
| _, Some v => Some v
| Some v, _ => Some v
| _, _ => None
end
end.
Definition includes_setpred (bb: list (list instr)) :=
existsb_val (existsb_val (fun x => match x with RBsetpred a _ _ _ => Some a | _ => None end)) bb.
Definition add_bb (should_split: bool) (i: list (list instr))
(bbc: list (list (list instr)) * list (list (list instr))) :=
match bbc with
| (a, b) => if should_split then (a, i::b) else (i::a, b)
end.
Fixpoint first_split (saw_pred: bool) (bb: bb) :=
match bb with
| a :: b =>
match includes_setpred a with
| Some v =>
let (_, res) := first_split true b in
(Some v, add_bb saw_pred a res)
| _ =>
let (v, res) := first_split saw_pred b in
(v, add_bb saw_pred a res)
end
| nil => (None, (nil, nil))
end.
Definition split_bb (fresh: node) (b: bb) : bb * bb * bb :=
match first_split false b with
| (Some p, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
| (None, (bb1, bb2)) => (bb1 ++ bb2, nil, nil)
end.
Definition transf_function (f: function) : function := f.
Definition transf_fundef (fd: fundef) : fundef :=
transf_fundef transf_function fd.
Definition transf_program (p: program) : program :=
transform_program transf_fundef p.
|
