Revision c825868a
Added by Xavier Thirioux over 10 years ago
| src/options.ml | ||
|---|---|---|
| 32 | 32 |
let witnesses = ref false |
| 33 | 33 |
let optimization = ref 2 |
| 34 | 34 |
let lusi = ref false |
| 35 |
let print_reuse = ref false |
|
| 35 | 36 |
|
| 36 | 37 |
let horntraces = ref false |
| 37 | 38 |
let horn_cex = ref false |
| ... | ... | |
| 55 | 56 |
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend."; |
| 56 | 57 |
"-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)"; |
| 57 | 58 |
"-horn-queries", Arg.Unit (fun () -> output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)"; |
| 59 |
"-print_reuse", Arg.Set print_reuse, "prints variable reuse policy"; |
|
| 58 | 60 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
| 59 | 61 |
"-inline", Arg.Set global_inline, "inline all node calls (require a main node)"; |
| 60 | 62 |
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation"; |
| src/scheduling.ml | ||
|---|---|---|
| 153 | 153 |
let unused = Liveness.compute_unused_variables n gg in |
| 154 | 154 |
let fanin = Liveness.compute_fanin n gg in |
| 155 | 155 |
|
| 156 |
let disjoint = Disjunction.clock_disjoint_map node_vars in |
|
| 157 |
|
|
| 158 |
Log.report ~level:3 |
|
| 159 |
(fun fmt -> |
|
| 160 |
Format.fprintf fmt |
|
| 161 |
"clock disjoint map for node %s: %a" |
|
| 162 |
n'.node_id |
|
| 163 |
Disjunction.pp_disjoint_map disjoint |
|
| 164 |
); |
|
| 165 |
|
|
| 166 |
let reuse = Liveness.compute_reuse_policy n sort disjoint gg in |
|
| 167 |
|
|
| 156 |
let (disjoint, reuse) = |
|
| 157 |
if !Options.optimization >= 3 |
|
| 158 |
then |
|
| 159 |
let disjoint = Disjunction.clock_disjoint_map node_vars in |
|
| 160 |
(disjoint, |
|
| 161 |
Liveness.compute_reuse_policy n sort disjoint gg) |
|
| 162 |
else |
|
| 163 |
(Hashtbl.create 1, |
|
| 164 |
Hashtbl.create 1) in |
|
| 165 |
|
|
| 166 |
if !Options.print_reuse |
|
| 167 |
then |
|
| 168 |
begin |
|
| 169 |
Log.report ~level:0 |
|
| 170 |
(fun fmt -> |
|
| 171 |
Format.fprintf fmt |
|
| 172 |
"OPT:clock disjoint map for node %s: %a" |
|
| 173 |
n'.node_id |
|
| 174 |
Disjunction.pp_disjoint_map disjoint |
|
| 175 |
); |
|
| 176 |
Log.report ~level:0 |
|
| 177 |
(fun fmt -> |
|
| 178 |
Format.fprintf fmt |
|
| 179 |
"OPT:reuse policy for node %s: %a" |
|
| 180 |
n'.node_id |
|
| 181 |
Liveness.pp_reuse_policy reuse |
|
| 182 |
); |
|
| 183 |
end; |
|
| 168 | 184 |
n', { schedule = sort; unused_vars = unused; fanin_table = fanin; reuse_table = reuse }
|
| 169 | 185 |
with (Causality.Cycle vl) as exc -> |
| 170 | 186 |
let vl = filter_original n vl in |
Also available in: Unified diff
added a new option -print_reuse that prints clock disjoint variables and reuse policy.
useful for debugging and carrying correctness proofs to the C code level.
non trivial result only when option -O 3 or above is activated.