## lustrec/src/tools/tiny/tiny_utils.ml @ ca7ff3f7

1 | f0195e96 | ploc | module Ast = Tiny.Ast |
---|---|---|---|

2 | |||

3 | 58fd528a | ploc | let gen_loc () = Tiny.Location.dummy () |

4 | f0195e96 | ploc | |

5 | ca7ff3f7 | Lélio Brun | 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 | |||

12 | f0195e96 | ploc | let ltyp_to_ttyp t = |

13 | if Types.is_real_type t then Tiny.Ast.RealT |
||

14 | else if Types.is_int_type t then Tiny.Ast.IntT |
||

15 | else if Types.is_bool_type t then Tiny.Ast.BoolT |
||

16 | ca7ff3f7 | Lélio Brun | else assert false |

17 | ```
(* not covered yet *)
``` |
||

18 | f0195e96 | ploc | |

19 | let cst_bool loc b = |
||

20 | ca7ff3f7 | Lélio Brun | ```
{
``` |

21 | Ast.expr_desc = |
||

22 | (if b then Ast.Cst (Q.of_int 1, "true") |
||

23 | else Ast.Cst (Q.of_int 0, "false")); |
||

24 | f0195e96 | ploc | expr_loc = loc; |

25 | ca7ff3f7 | Lélio Brun | expr_type = Ast.BoolT; |

26 | ```
}
``` |
||

27 | 58fd528a | ploc | |

28 | let cst_num loc t q = |
||

29 | ca7ff3f7 | Lélio Brun | { Ast.expr_desc = Ast.Cst (q, Q.to_string q); expr_loc = loc; expr_type = t } |

30 | |||

31 | f0195e96 | ploc | let rec real_to_q man exp = |

32 | ca7ff3f7 | Lélio Brun | 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) |
||

36 | f0195e96 | ploc | |

37 | let instr_loc i = |
||

38 | match i.Machine_code_types.lustre_eq with |
||

39 | ca7ff3f7 | Lélio Brun | | None -> |

40 | gen_loc () |
||

41 | | Some eq -> |
||

42 | lloc_to_tloc eq.eq_loc |
||

43 | |||

44 | f0195e96 | ploc | let rec lval_to_texpr loc _val = |

45 | ca7ff3f7 | Lélio Brun | let build d v = Ast.{ expr_desc = d; expr_loc = gen_loc (); expr_type = v } in |

46 | f0195e96 | ploc | let new_desc = |

47 | match _val.Machine_code_types.value_desc with |
||

48 | ca7ff3f7 | Lélio Brun | | 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 *)
``` |
||

95 | f0195e96 | ploc | ```
in
``` |

96 | build new_desc (ltyp_to_ttyp _val.value_type) |
||

97 | |||

98 | let machine_body_to_ast init m = |
||

99 | let init_var = ref None in |
||

100 | let rec guarded_expr_to_stm loc te guarded_instrs = |
||

101 | match guarded_instrs with |
||

102 | ca7ff3f7 | Lélio Brun | | [] -> |

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) |
||

130 | f0195e96 | ploc | and instr_to_stm i = |

131 | let loc = instr_loc i in |
||

132 | match i.instr_desc with |
||

133 | | MLocalAssign (v, e) | MStateAssign (v, e) -> |
||

134 | ca7ff3f7 | Lélio Brun | Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e) |

135 | | MBranch (e, guarded_instrs) -> |
||

136 | f0195e96 | ploc | let te = lval_to_texpr loc e in |

137 | guarded_expr_to_stm loc te guarded_instrs |
||

138 | | MStep (ol, id, args) -> |
||

139 | ca7ff3f7 | Lélio Brun | 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 |
||

158 | f0195e96 | ploc | and instrl_to_stm il = |

159 | match il with |
||

160 | ca7ff3f7 | Lélio Brun | | [] -> |

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) |
||

167 | f0195e96 | ploc | ```
in
``` |

168 | ca7ff3f7 | Lélio Brun | instrl_to_stm m.Machine_code_types.mstep.step_instrs |

169 | f0195e96 | ploc | |

170 | 58fd528a | ploc | let read_var bounds_opt v = |

171 | f0195e96 | ploc | let min, max = |

172 | match bounds_opt with |
||

173 | ca7ff3f7 | Lélio Brun | | Some (min, max) -> |

174 | min, max |
||

175 | | None -> |
||

176 | (Q.of_int (-1), "-1"), (Q.of_int 1, "1") |
||

177 | f0195e96 | ploc | ```
in
``` |

178 | ca7ff3f7 | Lélio Brun | let range = |

179 | ```
{
``` |
||

180 | Ast.expr_desc = Ast.Rand (min, max); |
||

181 | 58fd528a | ploc | expr_loc = gen_loc (); |

182 | ca7ff3f7 | Lélio Brun | expr_type = ltyp_to_ttyp v.Lustre_types.var_type; |

183 | f0195e96 | ploc | ```
}
``` |

184 | ```
in
``` |
||

185 | 58fd528a | ploc | Ast.Asn (gen_loc (), v.var_id, range) |

186 | ca7ff3f7 | Lélio Brun | |

187 | 58fd528a | ploc | let rec read_vars bounds_inputs vl = |

188 | f0195e96 | ploc | match vl with |

189 | ca7ff3f7 | Lélio Brun | | [] -> |

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 | |||

207 | f0195e96 | ploc | let machine_to_ast bounds_input m = |

208 | ca7ff3f7 | Lélio Brun | let read_vars = |

209 | read_vars bounds_input m.Machine_code_types.mstep.step_inputs |
||

210 | ```
in
``` |
||

211 | f0195e96 | ploc | let ast_loop_first = machine_body_to_ast true m in |

212 | let ast_loop_run = machine_body_to_ast false m in |
||

213 | 58fd528a | ploc | let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in |

214 | ca7ff3f7 | Lélio Brun | 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 | |||

219 | f0195e96 | ploc | let machine_to_env m = |

220 | ca7ff3f7 | Lélio Brun | List.fold_left |

221 | (fun accu v -> |
||

222 | let typ = ltyp_to_ttyp v.Lustre_types.var_type in |
||

223 | f0195e96 | ploc | Ast.VarSet.add (v.var_id, typ) accu) |

224 | Ast.VarSet.empty |
||

225 | (Machine_code_common.machine_vars m) |