Revision 79614a15
src/backends/C/c_backend_common.ml | ||
---|---|---|
92 | 92 |
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id |
93 | 93 |
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id |
94 | 94 |
|
95 |
let pp_c_dimension fmt d = |
|
96 |
fprintf fmt "%a" Dimension.pp_dimension d |
|
95 |
let rec pp_c_dimension fmt dim = |
|
96 |
match dim.Dimension.dim_desc with |
|
97 |
| Dident id -> |
|
98 |
fprintf fmt "%s" id |
|
99 |
| Dint i -> |
|
100 |
fprintf fmt "%d" i |
|
101 |
| Dbool b -> |
|
102 |
fprintf fmt "%B" b |
|
103 |
| Dite (i, t, e) -> |
|
104 |
fprintf fmt "((%a)?%a:%a)" |
|
105 |
pp_c_dimension i pp_c_dimension t pp_c_dimension e |
|
106 |
| Dappl (f, args) -> |
|
107 |
fprintf fmt "%a" (Basic_library.pp_c f pp_c_dimension) args |
|
108 |
| Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim' |
|
109 |
| Dvar -> fprintf fmt "_%s" (Utils.name_of_dimension dim.dim_id) |
|
110 |
| Dunivar -> fprintf fmt "'%s" (Utils.name_of_dimension dim.dim_id) |
|
97 | 111 |
|
98 | 112 |
let is_basic_c_type t = |
99 | 113 |
match (Types.repr t).Types.tdesc with |
... | ... | |
119 | 133 |
| Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix |
120 | 134 |
| Types.Tconst ty -> fprintf fmt "%s %s" ty var |
121 | 135 |
| Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var |
122 |
| _ -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false |
|
136 |
| _ -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
|
|
123 | 137 |
in aux t (fun fmt () -> ()) |
124 | 138 |
|
125 | 139 |
let rec pp_c_initialize fmt t = |
src/backends/C/c_backend_src.ml | ||
---|---|---|
30 | 30 |
(* Instruction Printing functions *) |
31 | 31 |
(********************************************************************************************) |
32 | 32 |
|
33 |
|
|
33 | 34 |
(* Computes the depth to which multi-dimension array assignments should be expanded. |
34 | 35 |
It equals the maximum number of nested static array constructions accessible from root [v]. |
35 | 36 |
*) |
... | ... | |
101 | 102 |
List.partition (function (d, LInt _) -> true | _ -> false) loop_vars |
102 | 103 |
in |
103 | 104 |
var_loops @ int_loops |
104 |
|
|
105 |
|
|
105 | 106 |
(* Prints a one loop variable suffix for arrays *) |
106 |
let pp_loop_var fmt lv = |
|
107 |
let pp_loop_var pp_value fmt lv =
|
|
107 | 108 |
match snd lv with |
108 | 109 |
| LVar v -> fprintf fmt "[%s]" v |
109 | 110 |
| LInt r -> fprintf fmt "[%d]" !r |
110 |
| LAcc i -> fprintf fmt "[%a]" pp_val i
|
|
111 |
| LAcc i -> fprintf fmt "[%a]" (pp_c_val "" pp_value) i
|
|
111 | 112 |
|
112 | 113 |
(* Prints a suffix of loop variables for arrays *) |
113 |
let pp_suffix fmt loop_vars = |
|
114 |
Utils.fprintf_list ~sep:"" pp_loop_var fmt loop_vars
|
|
114 |
let pp_suffix pp_value fmt loop_vars =
|
|
115 |
Utils.fprintf_list ~sep:"" (pp_loop_var pp_value) fmt loop_vars
|
|
115 | 116 |
|
116 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
|
117 |
let rec pp_value_suffix self loop_vars pp_value fmt value = |
|
117 |
(* Prints a value expression [v], with internal function calls only. |
|
118 |
[pp_var] is a printer for variables (typically [pp_c_var_read]), |
|
119 |
but an offset suffix may be added for array variables |
|
120 |
*) |
|
121 |
(* Prints a constant value before a suffix (needs casting) *) |
|
122 |
let rec pp_c_const_suffix var_type fmt c = |
|
123 |
match c with |
|
124 |
| Const_int i -> pp_print_int fmt i |
|
125 |
| Const_real r -> pp_print_string fmt r |
|
126 |
| Const_float r -> pp_print_float fmt r |
|
127 |
| Const_tag t -> pp_c_tag fmt t |
|
128 |
| Const_array ca -> let var_type = Types.array_element_type var_type in |
|
129 |
fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca |
|
130 |
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)) fl |
|
131 |
| Const_string _ -> assert false (* string occurs in annotations not in C *) |
|
132 |
|
|
133 |
|
|
134 |
(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *) |
|
135 |
let rec pp_value_suffix self var_type loop_vars pp_value fmt value = |
|
136 |
(*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*) |
|
118 | 137 |
match loop_vars, value with |
138 |
| (x, LAcc i) :: q, _ when is_const_index i -> |
|
139 |
let r = ref (Dimension.size_const_dimension (Machine_code.dimension_of_value i)) in |
|
140 |
pp_value_suffix self var_type ((x, LInt r)::q) pp_value fmt value |
|
141 |
| (_, LInt r) :: q, Cst (Const_array cl) -> |
|
142 |
let var_type = Types.array_element_type var_type in |
|
143 |
pp_value_suffix self var_type q pp_value fmt (Cst (List.nth cl !r)) |
|
119 | 144 |
| (_, LInt r) :: q, Array vl -> |
120 |
pp_value_suffix self q pp_value fmt (List.nth vl !r) |
|
145 |
let var_type = Types.array_element_type var_type in |
|
146 |
pp_value_suffix self var_type q pp_value fmt (List.nth vl !r) |
|
147 |
| loop_var :: q, Array vl -> |
|
148 |
let var_type = Types.array_element_type var_type in |
|
149 |
Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type q pp_value)) vl (pp_suffix pp_value) [loop_var] |
|
121 | 150 |
| _ :: q, Power (v, n) -> |
122 |
pp_value_suffix self q pp_value fmt v |
|
151 |
pp_value_suffix self var_type q pp_value fmt v
|
|
123 | 152 |
| _ , Fun (n, vl) -> |
124 |
Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl |
|
153 |
Basic_library.pp_c n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
|
|
125 | 154 |
| _ , Access (v, i) -> |
126 |
pp_value_suffix self ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v |
|
127 |
| _ , _ -> |
|
128 |
let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in |
|
129 |
pp_c_val self pp_var_suffix fmt value |
|
155 |
let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in |
|
156 |
pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v |
|
157 |
| _ , LocalVar v -> Format.fprintf fmt "%a%a" pp_value v (pp_suffix pp_value) loop_vars |
|
158 |
| _ , StateVar v -> |
|
159 |
(* array memory vars are represented by an indirection to a local var with the right type, |
|
160 |
in order to avoid casting everywhere. *) |
|
161 |
if Types.is_array_type v.var_type |
|
162 |
then Format.fprintf fmt "%a%a" pp_value v (pp_suffix pp_value) loop_vars |
|
163 |
else Format.fprintf fmt "%s->_reg.%a%a" self pp_value v (pp_suffix pp_value) loop_vars |
|
164 |
| _ , Cst cst -> pp_c_const_suffix var_type fmt cst |
|
165 |
| _ , _ -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type Machine_code.pp_val value (pp_suffix pp_value) loop_vars; assert false) |
|
130 | 166 |
|
131 | 167 |
(* type_directed assignment: array vs. statically sized type |
132 | 168 |
- [var_type]: type of variable to be assigned |
... | ... | |
157 | 193 |
match vars with |
158 | 194 |
| [] -> |
159 | 195 |
fprintf fmt "%a = %a;" |
160 |
(pp_value_suffix self loop_vars pp_var) var_name |
|
161 |
(pp_value_suffix self loop_vars pp_var) value |
|
196 |
(pp_value_suffix self var_type loop_vars pp_var) var_name
|
|
197 |
(pp_value_suffix self var_type loop_vars pp_var) value
|
|
162 | 198 |
| (d, LVar i) :: q -> |
163 | 199 |
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*) |
164 | 200 |
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}" |
src/basic_library.ml | ||
---|---|---|
127 | 127 |
| "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2 |
128 | 128 |
| "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2 |
129 | 129 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
130 |
| _ -> failwith i
|
|
130 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
|
|
131 | 131 |
|
132 | 132 |
let pp_java i pp_val fmt vl = |
133 | 133 |
match i, vl with |
... | ... | |
140 | 140 |
| "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 |
141 | 141 |
| "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 |
142 | 142 |
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 |
143 |
| _ -> assert false
|
|
143 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false)
|
|
144 | 144 |
|
145 | 145 |
let pp_horn i pp_val fmt vl = |
146 | 146 |
match i, vl with |
... | ... | |
158 | 158 |
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 |
159 | 159 |
| "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2 |
160 | 160 |
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 |
161 |
| _ -> assert false
|
|
161 |
| _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
|
|
162 | 162 |
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 |
163 | 163 |
|
164 | 164 |
*) |
src/causality.ml | ||
---|---|---|
216 | 216 |
| Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g) |
217 | 217 |
| Expr_pre e -> add_dep true lhs e g |
218 | 218 |
| Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g) |
219 |
| Expr_access (e1, _)
|
|
220 |
| Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
|
|
219 |
| Expr_access (e1, d)
|
|
220 |
| Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
|
|
221 | 221 |
| Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g |
222 | 222 |
| Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g |
223 | 223 |
| Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g) |
src/lustreSpec.ml | ||
---|---|---|
132 | 132 |
behaviors: (string * eexpr list * eexpr list * Location.t) list; |
133 | 133 |
spec_loc: Location.t; |
134 | 134 |
} |
135 |
|
|
136 |
type offset = |
|
137 |
| Index of Dimension.dim_expr |
|
138 |
| Field of label |
|
139 |
|
|
135 | 140 |
type assert_t = |
136 | 141 |
{ |
137 | 142 |
assert_expr: expr; |
src/main_lustre_compiler.ml | ||
---|---|---|
230 | 230 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,"); |
231 | 231 |
let machine_code = Machine_code.translate_prog prog node_schs in |
232 | 232 |
|
233 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," |
|
234 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
|
235 |
machine_code); |
|
236 |
|
|
233 | 237 |
(* Optimize machine code *) |
234 | 238 |
let machine_code = |
235 | 239 |
if !Options.optimization >= 4 && !Options.output <> "horn" then |
... | ... | |
241 | 245 |
machine_code |
242 | 246 |
in |
243 | 247 |
|
244 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," |
|
245 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
|
246 |
machine_code); |
|
247 |
|
|
248 | 248 |
(* Optimize machine code *) |
249 | 249 |
let machine_code = |
250 | 250 |
if !Options.optimization >= 2 && !Options.output <> "horn" then |
... | ... | |
266 | 266 |
machine_code |
267 | 267 |
in |
268 | 268 |
|
269 |
if !Options.optimization >= 2 then |
|
270 |
begin |
|
271 |
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," |
|
272 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
|
273 |
machine_code); |
|
274 |
end; |
|
269 | 275 |
|
270 | 276 |
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," |
271 | 277 |
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine) |
src/optimize_machine.ml | ||
---|---|---|
16 | 16 |
open Machine_code |
17 | 17 |
open Dimension |
18 | 18 |
|
19 |
(* Some optimizations may yield denormalized values. Similar to normalize_expr *) |
|
20 |
(* |
|
21 |
let normalize_value v = |
|
22 |
let rec norm_cst offset cst = |
|
23 |
match cst, offset with |
|
24 |
| Const_int _ , _ |
|
25 |
| Const_real _ , _ |
|
26 |
| Const_float _ , _ -> cst |
|
27 |
| Const_array args, Index i::q -> if Dimension.is_dimension_const |
|
28 |
| Const_tag of label |
|
29 |
| Const_string of string (* used only for annotations *) |
|
30 |
| Const_struct of (label * constant) list |
|
31 |
let rec norm_value offset v = |
|
32 |
match v with |
|
33 |
| Cst _ |
|
34 |
| LocalVar _ |
|
35 |
| StateVar _ -> v |
|
36 |
| Fun (id, args) -> Fun (id, List.map normalize_value args) |
|
37 |
| Array args -> Array List.map normalize_value args |
|
38 |
| Access of value_t * value_t |
|
39 |
| Power of value_t * value_t |
|
40 |
in norm [] v |
|
41 |
*) |
|
19 | 42 |
let pp_elim fmt elim = |
20 | 43 |
begin |
21 | 44 |
Format.fprintf fmt "{ /* elim table: */@."; |
src/parser_lustre.mly | ||
---|---|---|
257 | 257 |
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) } |
258 | 258 |
|
259 | 259 |
array_typ_decl: |
260 |
{ fun typ -> typ }
|
|
260 |
%prec POWER { fun typ -> typ }
|
|
261 | 261 |
| POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) } |
262 | 262 |
|
263 | 263 |
typeconst: |
src/types.ml | ||
---|---|---|
251 | 251 |
| Tstatic (_, ty') -> is_struct_type ty' |
252 | 252 |
| _ -> false |
253 | 253 |
|
254 |
let struct_field_type ty field = |
|
255 |
match (dynamic_type ty).tdesc with |
|
256 |
| Tstruct fields -> |
|
257 |
(try |
|
258 |
List.assoc field fields |
|
259 |
with Not_found -> assert false) |
|
260 |
| _ -> assert false |
|
261 |
|
|
254 | 262 |
let rec is_array_type ty = |
255 | 263 |
match (repr ty).tdesc with |
256 | 264 |
| Tarray _ -> true |
Also available in: Unified diff