Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/tiny/tiny_utils.ml | ||
---|---|---|
1 |
|
|
2 | 1 |
module Ast = Tiny.Ast |
3 | 2 |
|
4 | 3 |
let gen_loc () = Tiny.Location.dummy () |
5 |
|
|
6 |
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Location.loc_start loc.Location.loc_end |
|
7 |
|
|
8 |
let tloc_to_lloc loc = assert false (*Location.dummy_loc (*TODO*) *) |
|
9 | 4 |
|
10 |
|
|
5 |
let lloc_to_tloc loc = |
|
6 |
Tiny.Location.location_of_positions loc.Location.loc_start |
|
7 |
loc.Location.loc_end |
|
8 |
|
|
9 |
let tloc_to_lloc loc = assert false |
|
10 |
(*Location.dummy_loc (*TODO*) *) |
|
11 |
|
|
11 | 12 |
let ltyp_to_ttyp t = |
12 | 13 |
if Types.is_real_type t then Tiny.Ast.RealT |
13 | 14 |
else if Types.is_int_type t then Tiny.Ast.IntT |
14 | 15 |
else if Types.is_bool_type t then Tiny.Ast.BoolT |
15 |
else assert false (* not covered yet *) |
|
16 |
else assert false |
|
17 |
(* not covered yet *) |
|
16 | 18 |
|
17 | 19 |
let cst_bool loc b = |
18 |
{ Ast.expr_desc = |
|
19 |
if b then |
|
20 |
Ast.Cst(Q.of_int 1, "true") |
|
21 |
else |
|
22 |
Ast.Cst(Q.of_int 0, "false"); |
|
20 |
{ |
|
21 |
Ast.expr_desc = |
|
22 |
(if b then Ast.Cst (Q.of_int 1, "true") |
|
23 |
else Ast.Cst (Q.of_int 0, "false")); |
|
23 | 24 |
expr_loc = loc; |
24 |
expr_type = Ast.BoolT } |
|
25 |
expr_type = Ast.BoolT; |
|
26 |
} |
|
25 | 27 |
|
26 | 28 |
let cst_num loc t q = |
27 |
{ Ast.expr_desc = |
|
28 |
Ast.Cst(q, Q.to_string q); |
|
29 |
expr_loc = loc; |
|
30 |
expr_type = t } |
|
31 |
|
|
29 |
{ Ast.expr_desc = Ast.Cst (q, Q.to_string q); expr_loc = loc; expr_type = t } |
|
30 |
|
|
32 | 31 |
let rec real_to_q man exp = |
33 |
if exp = 0 then |
|
34 |
Q.of_string (Num.string_of_num man) |
|
35 |
else |
|
36 |
if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10) |
|
37 |
else (* if exp<0 then *) |
|
38 |
Q.mul |
|
39 |
(real_to_q man (exp+1)) |
|
40 |
(Q.of_int 10) |
|
32 |
if exp = 0 then Q.of_string (Num.string_of_num man) |
|
33 |
else if exp > 0 then Q.div (real_to_q man (exp - 1)) (Q.of_int 10) |
|
34 |
else (* if exp<0 then *) |
|
35 |
Q.mul (real_to_q man (exp + 1)) (Q.of_int 10) |
|
41 | 36 |
|
42 | 37 |
let instr_loc i = |
43 | 38 |
match i.Machine_code_types.lustre_eq with |
44 |
| None -> gen_loc () |
|
45 |
| Some eq -> lloc_to_tloc eq.eq_loc |
|
46 |
|
|
39 |
| None -> |
|
40 |
gen_loc () |
|
41 |
| Some eq -> |
|
42 |
lloc_to_tloc eq.eq_loc |
|
43 |
|
|
47 | 44 |
let rec lval_to_texpr loc _val = |
48 |
let build d v = |
|
49 |
Ast.{ expr_desc = d; |
|
50 |
expr_loc = gen_loc (); |
|
51 |
expr_type = v } |
|
52 |
in |
|
45 |
let build d v = Ast.{ expr_desc = d; expr_loc = gen_loc (); expr_type = v } in |
|
53 | 46 |
let new_desc = |
54 | 47 |
match _val.Machine_code_types.value_desc with |
55 |
| Machine_code_types.Cst cst -> ( |
|
56 |
match cst with |
|
57 |
Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n) |
|
58 |
| Const_real r -> Ast.Cst (Real.to_q r, Real.to_string r) |
|
59 |
| _ -> assert false |
|
60 |
) |
|
61 |
|
|
62 |
| Var v -> Ast.Var (v.var_id) |
|
63 |
| Fun (op, vl) -> |
|
64 |
let t_arg = match vl with |
|
65 |
| hd::_ -> ltyp_to_ttyp hd.value_type |
|
66 |
| _ -> assert false |
|
67 |
in |
|
68 |
( |
|
69 |
match op, List.map (lval_to_texpr loc) vl with |
|
70 |
| "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2) |
|
71 |
| "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2) |
|
72 |
| "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2) |
|
73 |
| "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2) |
|
74 |
| "<", [v1;v2] -> |
|
75 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict) |
|
76 |
| "<=", [v1;v2] -> |
|
77 |
Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose) |
|
78 |
| ">", [v1;v2] -> |
|
79 |
Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict) |
|
80 |
| ">=", [v1;v2] -> |
|
81 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose) |
|
82 |
| "=", [v1;v2] -> |
|
83 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero) |
|
84 |
| "!=", [v1;v2] -> |
|
85 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero) |
|
86 |
| "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1) |
|
87 |
| _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false |
|
88 |
) |
|
89 |
| _ -> assert false (* no array. access or power *) |
|
48 |
| Machine_code_types.Cst cst -> ( |
|
49 |
match cst with |
|
50 |
| Lustre_types.Const_int n -> |
|
51 |
Ast.Cst (Q.of_int n, string_of_int n) |
|
52 |
| Const_real r -> |
|
53 |
Ast.Cst (Real.to_q r, Real.to_string r) |
|
54 |
| _ -> |
|
55 |
assert false) |
|
56 |
| Var v -> |
|
57 |
Ast.Var v.var_id |
|
58 |
| Fun (op, vl) -> ( |
|
59 |
let t_arg = |
|
60 |
match vl with |
|
61 |
| hd :: _ -> |
|
62 |
ltyp_to_ttyp hd.value_type |
|
63 |
| _ -> |
|
64 |
assert false |
|
65 |
in |
|
66 |
match op, List.map (lval_to_texpr loc) vl with |
|
67 |
| "+", [ v1; v2 ] -> |
|
68 |
Ast.Binop (Ast.Plus, v1, v2) |
|
69 |
| "-", [ v1; v2 ] -> |
|
70 |
Ast.Binop (Ast.Minus, v1, v2) |
|
71 |
| "*", [ v1; v2 ] -> |
|
72 |
Ast.Binop (Ast.Times, v1, v2) |
|
73 |
| "/", [ v1; v2 ] -> |
|
74 |
Ast.Binop (Ast.Div, v1, v2) |
|
75 |
| "<", [ v1; v2 ] -> |
|
76 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict) |
|
77 |
| "<=", [ v1; v2 ] -> |
|
78 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose) |
|
79 |
| ">", [ v1; v2 ] -> |
|
80 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict) |
|
81 |
| ">=", [ v1; v2 ] -> |
|
82 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose) |
|
83 |
| "=", [ v1; v2 ] -> |
|
84 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero) |
|
85 |
| "!=", [ v1; v2 ] -> |
|
86 |
Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero) |
|
87 |
| "uminus", [ v1 ] -> |
|
88 |
Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1) |
|
89 |
| _ -> |
|
90 |
Format.eprintf "No tiny translation for operator %s@.@?" op; |
|
91 |
assert false) |
|
92 |
| _ -> |
|
93 |
assert false |
|
94 |
(* no array. access or power *) |
|
90 | 95 |
in |
91 | 96 |
build new_desc (ltyp_to_ttyp _val.value_type) |
92 | 97 |
|
93 |
|
|
94 | 98 |
let machine_body_to_ast init m = |
95 | 99 |
let init_var = ref None in |
96 | 100 |
let rec guarded_expr_to_stm loc te guarded_instrs = |
97 | 101 |
match guarded_instrs with |
98 |
| [] -> assert false |
|
99 |
| [_,il] -> instrl_to_stm il |
|
100 |
| (label, il)::tl -> |
|
101 |
let stmt = instrl_to_stm il in |
|
102 |
let guard= match label with |
|
103 |
"true" -> te |
|
104 |
| "false" -> Ast.neg_guard te |
|
105 |
| _ -> assert false (* TODO: don't deal with non boolean |
|
106 |
guards. Could just treturn true and |
|
107 |
over-approximate behavior *) |
|
108 |
in |
|
109 |
if (match !init_var, te.Ast.expr_desc with |
|
110 |
| Some v, Var v2 -> v = v2 |
|
111 |
| _ -> false) then |
|
112 |
instrl_to_stm ( |
|
113 |
if init then |
|
114 |
(List.assoc "true" guarded_instrs) |
|
115 |
else |
|
116 |
(List.assoc "false" guarded_instrs) |
|
117 |
) |
|
118 |
else |
|
119 |
Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl) |
|
102 |
| [] -> |
|
103 |
assert false |
|
104 |
| [ (_, il) ] -> |
|
105 |
instrl_to_stm il |
|
106 |
| (label, il) :: tl -> |
|
107 |
let stmt = instrl_to_stm il in |
|
108 |
let guard = |
|
109 |
match label with |
|
110 |
| "true" -> |
|
111 |
te |
|
112 |
| "false" -> |
|
113 |
Ast.neg_guard te |
|
114 |
| _ -> |
|
115 |
assert false |
|
116 |
(* TODO: don't deal with non boolean guards. Could just treturn true and |
|
117 |
over-approximate behavior *) |
|
118 |
in |
|
119 |
if |
|
120 |
match !init_var, te.Ast.expr_desc with |
|
121 |
| Some v, Var v2 -> |
|
122 |
v = v2 |
|
123 |
| _ -> |
|
124 |
false |
|
125 |
then |
|
126 |
instrl_to_stm |
|
127 |
(if init then List.assoc "true" guarded_instrs |
|
128 |
else List.assoc "false" guarded_instrs) |
|
129 |
else Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl) |
|
120 | 130 |
and instr_to_stm i = |
121 | 131 |
let loc = instr_loc i in |
122 | 132 |
match i.instr_desc with |
123 | 133 |
| MLocalAssign (v, e) | MStateAssign (v, e) -> |
124 |
Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
|
|
125 |
| MBranch (e, guarded_instrs) -> (
|
|
134 |
Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e) |
|
135 |
| MBranch (e, guarded_instrs) -> |
|
126 | 136 |
let te = lval_to_texpr loc e in |
127 | 137 |
guarded_expr_to_stm loc te guarded_instrs |
128 |
) |
|
129 | 138 |
| MStep (ol, id, args) -> |
130 |
if List.mem_assoc id m.Machine_code_types.minstances then |
|
131 |
let fun_name, _ = List.assoc id m.minstances in |
|
132 |
match Corelang.node_name fun_name, ol with |
|
133 |
| "_arrow", [o] -> ( |
|
134 |
init_var := Some o.var_id; |
|
135 |
Ast.Nop (loc); |
|
136 |
(* Ast.Asn (loc, o.var_id, |
|
137 |
* { expr_desc = if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false"); |
|
138 |
* expr_loc = loc; |
|
139 |
* expr_type = Ast.BoolT } |
|
140 |
* ) *) |
|
141 |
) |
|
142 |
| name, _ -> |
|
143 |
( |
|
144 |
Format.eprintf "No tiny translation for node call %s@.@?" name; |
|
145 |
assert false |
|
146 |
) |
|
147 |
else ( |
|
148 |
Format.eprintf "No tiny translation for node call %s@.@?" id; |
|
149 |
assert false |
|
150 |
) |
|
151 |
| MReset id |
|
152 |
| MNoReset id -> assert false (* no more calls or functions, ie. no reset *) |
|
153 |
| MComment s |
|
154 |
| MSpec s -> assert false |
|
139 |
if List.mem_assoc id m.Machine_code_types.minstances then ( |
|
140 |
let fun_name, _ = List.assoc id m.minstances in |
|
141 |
match Corelang.node_name fun_name, ol with |
|
142 |
| "_arrow", [ o ] -> |
|
143 |
init_var := Some o.var_id; |
|
144 |
Ast.Nop loc |
|
145 |
(* Ast.Asn (loc, o.var_id, * { expr_desc = if init then Ast.Cst(Q.of_int |
|
146 |
1, "true") else Ast.Cst(Q.of_int 0, "false"); * expr_loc = loc; * |
|
147 |
expr_type = Ast.BoolT } * ) *) |
|
148 |
| name, _ -> |
|
149 |
Format.eprintf "No tiny translation for node call %s@.@?" name; |
|
150 |
assert false) |
|
151 |
else ( |
|
152 |
Format.eprintf "No tiny translation for node call %s@.@?" id; |
|
153 |
assert false) |
|
154 |
| MReset id | MNoReset id -> |
|
155 |
assert false (* no more calls or functions, ie. no reset *) |
|
156 |
| MComment s | MSpec s -> |
|
157 |
assert false |
|
155 | 158 |
and instrl_to_stm il = |
156 | 159 |
match il with |
157 |
[] -> assert false |
|
158 |
| [i] -> instr_to_stm i |
|
159 |
| i::il -> |
|
160 |
let i' = instr_to_stm i in |
|
161 |
Ast.Seq (gen_loc (), i', (instrl_to_stm il)) |
|
160 |
| [] -> |
|
161 |
assert false |
|
162 |
| [ i ] -> |
|
163 |
instr_to_stm i |
|
164 |
| i :: il -> |
|
165 |
let i' = instr_to_stm i in |
|
166 |
Ast.Seq (gen_loc (), i', instrl_to_stm il) |
|
162 | 167 |
in |
163 |
instrl_to_stm m.Machine_code_types.mstep.step_instrs
|
|
168 |
instrl_to_stm m.Machine_code_types.mstep.step_instrs |
|
164 | 169 |
|
165 | 170 |
let read_var bounds_opt v = |
166 | 171 |
let min, max = |
167 | 172 |
match bounds_opt with |
168 |
Some (min,max) -> min, max |
|
169 |
| None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1") |
|
173 |
| Some (min, max) -> |
|
174 |
min, max |
|
175 |
| None -> |
|
176 |
(Q.of_int (-1), "-1"), (Q.of_int 1, "1") |
|
170 | 177 |
in |
171 |
let range = { |
|
172 |
Ast.expr_desc = Ast.Rand (min,max); |
|
178 |
let range = |
|
179 |
{ |
|
180 |
Ast.expr_desc = Ast.Rand (min, max); |
|
173 | 181 |
expr_loc = gen_loc (); |
174 |
expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
|
|
182 |
expr_type = ltyp_to_ttyp v.Lustre_types.var_type;
|
|
175 | 183 |
} |
176 | 184 |
in |
177 | 185 |
Ast.Asn (gen_loc (), v.var_id, range) |
178 |
|
|
186 |
|
|
179 | 187 |
let rec read_vars bounds_inputs vl = |
180 | 188 |
match vl with |
181 |
[] -> Ast.Nop (gen_loc ())
|
|
182 |
| [v] -> read_var
|
|
183 |
(if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
|
|
184 |
Some (List.assoc v.Lustre_types.var_id bounds_inputs)
|
|
185 |
else
|
|
186 |
None)
|
|
187 |
v
|
|
188 |
| v::tl ->
|
|
189 |
Ast.Seq (gen_loc (),
|
|
190 |
read_var
|
|
191 |
(if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
|
|
192 |
Some (List.assoc v.Lustre_types.var_id bounds_inputs)
|
|
193 |
else
|
|
194 |
None)
|
|
195 |
v,
|
|
196 |
read_vars bounds_inputs tl
|
|
197 |
) |
|
198 |
|
|
189 |
| [] ->
|
|
190 |
Ast.Nop (gen_loc ())
|
|
191 |
| [ v ] ->
|
|
192 |
read_var
|
|
193 |
(if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
|
|
194 |
Some (List.assoc v.Lustre_types.var_id bounds_inputs)
|
|
195 |
else None)
|
|
196 |
v
|
|
197 |
| v :: tl ->
|
|
198 |
Ast.Seq
|
|
199 |
( gen_loc (),
|
|
200 |
read_var
|
|
201 |
(if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
|
|
202 |
Some (List.assoc v.Lustre_types.var_id bounds_inputs)
|
|
203 |
else None)
|
|
204 |
v,
|
|
205 |
read_vars bounds_inputs tl )
|
|
206 |
|
|
199 | 207 |
let machine_to_ast bounds_input m = |
200 |
let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in |
|
208 |
let read_vars = |
|
209 |
read_vars bounds_input m.Machine_code_types.mstep.step_inputs |
|
210 |
in |
|
201 | 211 |
let ast_loop_first = machine_body_to_ast true m in |
202 | 212 |
let ast_loop_run = machine_body_to_ast false m in |
203 | 213 |
let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in |
204 |
let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in |
|
205 |
Ast.Seq (gen_loc (), read_vars, (Ast.Seq (gen_loc (), ast_loop_first, loop))) |
|
206 |
|
|
214 |
let loop = |
|
215 |
Ast.While (gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) |
|
216 |
in |
|
217 |
Ast.Seq (gen_loc (), read_vars, Ast.Seq (gen_loc (), ast_loop_first, loop)) |
|
218 |
|
|
207 | 219 |
let machine_to_env m = |
208 |
|
|
209 |
List.fold_left (fun accu v -> |
|
210 |
let typ = |
|
211 |
ltyp_to_ttyp (v.Lustre_types.var_type) |
|
212 |
in |
|
220 |
List.fold_left |
|
221 |
(fun accu v -> |
|
222 |
let typ = ltyp_to_ttyp v.Lustre_types.var_type in |
|
213 | 223 |
Ast.VarSet.add (v.var_id, typ) accu) |
214 | 224 |
Ast.VarSet.empty |
215 | 225 |
(Machine_code_common.machine_vars m) |
216 |
|
Also available in: Unified diff
reformatting