Revision 9a9058f4
Added by Pierre-Loïc Garoche over 5 years ago
| src/plugins/salsa/machine_salsa_opt.ml | ||
|---|---|---|
| 98 | 98 |
let fresh_id = "toto" in (* TODO more meaningful name *) |
| 99 | 99 |
|
| 100 | 100 |
let abstractEnv = RangesInt.to_abstract_env ranges in |
| 101 |
Format.eprintf "Launching analysis@.@?"; |
|
| 101 | 102 |
let new_e_salsa, e_val = |
| 102 | 103 |
Salsa.MainEPEG.transformExpression fresh_id e_salsa abstractEnv |
| 103 | 104 |
in |
| 105 |
Format.eprintf " Analysis done@.@?"; |
|
| 104 | 106 |
|
| 105 | 107 |
|
| 106 | 108 |
(* (\* Debug *\) *) |
| ... | ... | |
| 109 | 111 |
(* (Salsa.Print.printExpression new_e_salsa); *) |
| 110 | 112 |
(* (\* Debug *\) *) |
| 111 | 113 |
|
| 114 |
Format.eprintf " Computing range progress@.@?"; |
|
| 112 | 115 |
|
| 113 | 116 |
let old_val = Salsa.Analyzer.evalExpr e_salsa abstractEnv [] in |
| 114 | 117 |
let expr, expr_range = |
| ... | ... | |
| 119 | 122 |
); |
| 120 | 123 |
e_salsa, Some old_val |
| 121 | 124 |
) |
| 122 |
| true, false -> (
|
|
| 125 |
| false, true -> (
|
|
| 123 | 126 |
if !debug then Log.report ~level:2 (fun fmt -> |
| 124 | 127 |
Format.fprintf fmt "Improved!@ "; |
| 125 | 128 |
); |
| 126 | 129 |
new_e_salsa, Some e_val |
| 127 | 130 |
) |
| 128 |
| false, true -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; e_salsa, Some old_val |
|
| 129 |
|
|
| 130 |
| false, false -> |
|
| 131 |
Format.eprintf |
|
| 132 |
"Error; new range is not comparabe with old end. This should not happen!@.@?"; |
|
| 133 |
assert false |
|
| 131 |
| true, false -> Format.eprintf "CAREFUL --- new range is worse!. Restoring provided expression@ "; e_salsa, Some old_val |
|
| 132 |
|
|
| 133 |
| false, false -> ( |
|
| 134 |
Format.eprintf |
|
| 135 |
"Error; new range is not comparabe with old end. It may need some investigation!@.@?"; |
|
| 136 |
Format.eprintf "old: %a@.new: %a@.@?" |
|
| 137 |
RangesInt.pp_val old_val |
|
| 138 |
RangesInt.pp_val e_val; |
|
| 139 |
|
|
| 140 |
new_e_salsa, Some e_val |
|
| 141 |
(* assert false *) |
|
| 142 |
) |
|
| 134 | 143 |
in |
| 144 |
Format.eprintf " Computing range done@.@?"; |
|
| 145 |
|
|
| 135 | 146 |
if !debug then Log.report ~level:2 (fun fmt -> |
| 136 | 147 |
Format.fprintf fmt |
| 137 | 148 |
" @[<v>old_expr: @[<v 0>%s@ range: %a@]@ new_expr: @[<v 0>%s@ range: %a@]@ @]@ " |
Also available in: Unified diff
More work on Salsa plugin