Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / backends / tiny / tiny_utils.ml @ 9b0432bc

History | View | Annotate | Download (10.4 KB)

1 9b0432bc Corentin Lauverjat
open Lustrec
2
open Machine_code_types
3
open Format 
4
open Yojson
5
open Printers 
6 f0195e96 ploc
7
module Ast = Tiny.Ast
8
9 9b0432bc Corentin Lauverjat
type bound = {
10
  var_name: string;
11
  _type: string;[@key "type"]
12
  inf: string;
13
  sup: string
14
} [@@deriving yojson]
15
type bounds = bound list [@@deriving yojson]
16
17
18 58fd528a ploc
let gen_loc () = Tiny.Location.dummy ()
19
               
20 9c4cc944 Corentin Lauverjat
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Lustrec.Location.loc_start loc.Lustrec.Location.loc_end
21 f0195e96 ploc
                     
22 9c4cc944 Corentin Lauverjat
let tloc_to_lloc loc = assert false (*Lustrec.Location.dummy_loc (*TODO*) *)
23 f0195e96 ploc
24 9b0432bc Corentin Lauverjat
(* Take a List of Ast.stm (Tiny statements) and 
25
   make an Ast Seq node from the statements *)
26
let stmt_list_to_ast (stmt_list:Ast.stm list) = 
27
  let location_last_statement = gen_loc() in
28
  let stmt_seq = List.fold_right (fun stm ast -> Ast.Seq (gen_loc(), stm, ast)) 
29
  stmt_list (Ast.Nop location_last_statement) in 
30
  stmt_seq
31
32
(* Take a Lustre Type and return the corresponding Tiny type *)                     
33 f0195e96 ploc
let ltyp_to_ttyp t =
34 9c4cc944 Corentin Lauverjat
  if Lustrec.Types.is_real_type t then Tiny.Ast.RealT
35
  else if Lustrec.Types.is_int_type t then Tiny.Ast.IntT
36
  else if Lustrec.Types.is_bool_type t then Tiny.Ast.BoolT
37 f0195e96 ploc
  else assert false (* not covered yet *)
38
39 9b0432bc Corentin Lauverjat
(* Create a Tiny boolean constant *)
40
let cst_bool (loc:Tiny.Location.t) (b:bool) =
41 f0195e96 ploc
  { Ast.expr_desc =
42
      if b then
43
        Ast.Cst(Q.of_int 1, "true")
44
      else
45
        Ast.Cst(Q.of_int 0, "false");
46
    expr_loc = loc;
47
    expr_type = Ast.BoolT }
48 58fd528a ploc
49 9b0432bc Corentin Lauverjat
(* Create a Tiny numeric constant *)
50
let cst_num (loc:Tiny.Location.t) (t:Tiny.Ast.base_type) (q:Q.t) =
51 58fd528a ploc
{ Ast.expr_desc =
52
    Ast.Cst(q, Q.to_string q);
53
  expr_loc = loc;
54
  expr_type = t }
55 f0195e96 ploc
  
56
let rec real_to_q man exp =
57
  if exp = 0 then
58
        Q.of_string (Num.string_of_num man)
59
  else
60
    if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
61
    else (* if exp<0 then *)
62
      Q.mul
63
        (real_to_q man (exp+1))
64
        (Q.of_int 10)
65
66 9b0432bc Corentin Lauverjat
(* Take a Lustrec instruction and return a Tiny location *)
67 f0195e96 ploc
let instr_loc i =
68 9c4cc944 Corentin Lauverjat
  match i.Lustrec.Machine_code_types.lustre_eq with
69 58fd528a ploc
  | None -> gen_loc ()
70 f0195e96 ploc
  | Some eq -> lloc_to_tloc eq.eq_loc
71
             
72 9b0432bc Corentin Lauverjat
(* Convert a lustrec value to a Tiny expression *)
73 f0195e96 ploc
let rec lval_to_texpr loc _val =
74
  let build d v =
75
      Ast.{ expr_desc = d;
76 58fd528a ploc
            expr_loc = gen_loc ();
77 f0195e96 ploc
            expr_type = v }
78
  in
79
  let new_desc =
80 9c4cc944 Corentin Lauverjat
    match _val.Lustrec.Machine_code_types.value_desc with
81
  | Lustrec.Machine_code_types.Cst cst -> (
82 f0195e96 ploc
    match cst with
83 9c4cc944 Corentin Lauverjat
      Lustrec.Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
84
    | Const_real r -> Ast.Cst (Lustrec.Real.to_q r, Lustrec.Real.to_string r) 
85 9b0432bc Corentin Lauverjat
  | Const_array _ -> failwith "Const_array not yet supported"
86
  | Const_tag id -> (match id with 
87
    | "true" ->  Ast.Cst(Q.of_int 1,id) 
88
    | "false" -> Ast.Cst(Q.of_int 0, id)
89
    |_ -> failwith ("Const_tag "^ id^" not yet supported"))
90
  | Const_string _ -> failwith "Const_string not yet suported"
91
  | Const_modeid _ -> failwith "Const_modeid not yet supported"
92
  | Const_struct _ -> failwith "Const_struct not yet supported"
93 f0195e96 ploc
      | _ -> assert false
94
  )
95
     
96
  | Var v -> Ast.Var (v.var_id)
97
  | Fun (op, vl) ->
98
     let t_arg = match vl with
99
       | hd::_ -> ltyp_to_ttyp hd.value_type
100
       | _ -> assert false
101
     in
102
     (
103
       match op, List.map (lval_to_texpr loc) vl with
104
       | "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2)
105
       | "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2)
106
       | "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2)
107
       | "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2)
108
       | "<", [v1;v2] ->
109
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
110
       | "<=", [v1;v2] ->
111
          Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
112
       | ">", [v1;v2] ->
113
          Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
114
       | ">=", [v1;v2] ->
115
          Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
116
       | "=", [v1;v2] ->
117
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
118 9b0432bc Corentin Lauverjat
       | "equi", [v1;v2] ->
119
          (* generate an ast node based on 
120
            v1 <=> v2 if and only if v1 && v2 || (!v1 &&!v2) *)
121
          let tt = build (Ast.Binop (Ast.And,v1,v2)) BoolT and
122
           ff = build (Ast.Binop (Ast.And,(build (Ast.Unop (Ast.Not, v1)) BoolT),(build (Ast.Unop (Ast.Not, v2)) BoolT))) BoolT in
123
          Ast.Binop (Ast.Or, tt, ff)
124 f0195e96 ploc
       | "!=", [v1;v2] ->
125
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
126 58fd528a ploc
       | "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1)
127 9b0432bc Corentin Lauverjat
       | "not", [v1] -> Ast.Unop (Ast.Not, v1)
128
       | "&&", [v1;v2] -> Ast.Binop (Ast.And, v1, v2)
129
       | "||", [v1;v2] -> Ast.Binop (Ast.Or, v1, v2)
130 f0195e96 ploc
       | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
131
  )
132 9b0432bc Corentin Lauverjat
  | Array vl      -> failwith "array are not supported yet"
133
  | Access (t, i) -> failwith "acces not supported yet"
134
  | Power (v, n)  -> failwith "powser not supported yet"
135 f0195e96 ploc
  | _ -> assert false (* no array. access or power *)
136
  in
137
  build new_desc (ltyp_to_ttyp _val.value_type)
138
139
  
140
let machine_body_to_ast init m =
141
  let init_var = ref None in
142
  let rec guarded_expr_to_stm loc te guarded_instrs =
143
    match guarded_instrs with
144
    | [] -> assert false
145
    | [_,il] -> instrl_to_stm il
146
    | (label, il)::tl ->
147
       let stmt = instrl_to_stm il in
148
       let guard= match label with
149
           "true" -> te
150
         | "false" -> Ast.neg_guard te
151
         | _ -> assert false (* TODO: don't deal with non boolean
152
                                guards. Could just treturn true and
153
                                over-approximate behavior *)
154
       in
155
       if (match !init_var, te.Ast.expr_desc with
156
           | Some v, Var v2 -> v = v2
157
           | _ -> false) then 
158
         instrl_to_stm (
159
             if init then
160
               (List.assoc "true" guarded_instrs)
161
             else
162
               (List.assoc "false" guarded_instrs)
163
           )
164
       else
165
         Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl)
166
  and instr_to_stm i =
167
    let loc = instr_loc i in
168
    match i.instr_desc with
169
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
170
       Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
171
    | MBranch (e, guarded_instrs) -> (
172
      let te = lval_to_texpr loc e in
173
      guarded_expr_to_stm loc te guarded_instrs
174
    )
175
    | MStep (ol, id, args) ->
176 9c4cc944 Corentin Lauverjat
       if List.mem_assoc id m.Lustrec.Machine_code_types.minstances then
177 f0195e96 ploc
         let fun_name, _ = List.assoc id m.minstances in
178 9c4cc944 Corentin Lauverjat
         match Lustrec.Corelang.node_name fun_name, ol with
179 f0195e96 ploc
         | "_arrow", [o] -> (
180
           init_var := Some o.var_id;
181
           Ast.Nop (loc);
182
             (* Ast.Asn (loc, o.var_id, 
183
              *        { expr_desc =              if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false");
184
              *          expr_loc = loc;
185
              *          expr_type = Ast.BoolT }
186
              * ) *)
187
         )
188
         | name, _ -> 
189
            (
190
              Format.eprintf "No tiny translation for node call  %s@.@?" name;
191
              assert false
192
            )
193
       else (
194
         Format.eprintf "No tiny translation for node call  %s@.@?" id;
195
         assert false
196
       )
197
    | MReset id
198 9b0432bc Corentin Lauverjat
    | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
199 f0195e96 ploc
    | MComment s 
200
      | MSpec s -> assert false
201
  and instrl_to_stm il =
202
    match il with
203
      [] -> assert false
204
    | [i] -> instr_to_stm i
205
    | i::il ->
206
       let i' = instr_to_stm i in
207 58fd528a ploc
       Ast.Seq (gen_loc (), i', (instrl_to_stm il))
208 f0195e96 ploc
  in
209 9b0432bc Corentin Lauverjat
  let stmts_print_output =  List.map (fun (o:Lustre_types.var_decl)-> 
210
    let ast_variable =  Ast.{ expr_desc = Ast.Var(o.var_id);
211
            expr_loc = gen_loc ();
212
            expr_type =ltyp_to_ttyp o.var_type } in 
213
    (* printing_function_name = print_{bool/int/real} depending on the type of the variable *)
214
    let printing_function_name = (Format.asprintf "print_%a" Ast.pp_base_type (ltyp_to_ttyp o.var_type)) in 
215
     Ast.Asn (gen_loc(), "_ignore", 
216
        Ast.{ expr_desc = Ast.Call(printing_function_name ,[ast_variable]);
217
            expr_loc = gen_loc ();
218
            expr_type = Ast.BoolT }
219
      )
220
  ) m.mname.node_outputs |> stmt_list_to_ast in
221
  let translation = instrl_to_stm m.Lustrec.Machine_code_types.mstep.step_instrs in 
222
  Ast.Seq (gen_loc (), translation,stmts_print_output)
223 f0195e96 ploc
224 9b0432bc Corentin Lauverjat
 
225
226
227
228
229
230
let read_var bound v =
231
  (* TODO : manage boolean cases properly *)
232 f0195e96 ploc
  let range = {
233 9b0432bc Corentin Lauverjat
      Ast.expr_desc = Ast.Rand ((Q.of_string bound.inf, bound.inf),(Q.of_string bound.sup, bound.sup));
234 58fd528a ploc
      expr_loc = gen_loc ();
235 9c4cc944 Corentin Lauverjat
      expr_type = ltyp_to_ttyp (v.Lustrec.Lustre_types.var_type)
236 f0195e96 ploc
    }
237
  in
238 58fd528a ploc
  Ast.Asn (gen_loc (), v.var_id, range)
239 f0195e96 ploc
  
240 58fd528a ploc
let rec read_vars bounds_inputs vl =
241 9b0432bc Corentin Lauverjat
  let find_bound_of_var v  = 
242
      (match List.find_all (fun bound -> bound.var_name = Lustrec.Lustre_types.(v.var_id)) bounds_inputs with 
243
      | [] -> begin
244
        Log.report ~level:0 (fun fmt -> fprintf fmt ".. error %a is not bound @." pp_var v);
245
        exit 2
246
      end
247
      | [b] -> b
248
      | b::bs -> begin 
249
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. warning %a is bound multiple times ignoring constraints other than the first one @." pp_var v);
250
        b
251
      end
252
    ) 
253
  in 
254
  let reading_statements = List.map (fun v -> 
255
    let bound = find_bound_of_var v in 
256
    read_var bound v
257
  ) vl 
258
  in stmt_list_to_ast reading_statements;
259
(*
260
A type to encode the Lustre machine in the Tiny world
261
*)
262
type tiny_encoding = {
263
  ast:Ast.stm; 
264
  variables: Ast.VarSet.t; 
265
  location_beg_while: Tiny.Location.t; 
266
}
267
268
269 f0195e96 ploc
let machine_to_env m =
270 9b0432bc Corentin Lauverjat
    let var_set = List.fold_left (fun accu v ->
271 f0195e96 ploc
      let typ =
272 9c4cc944 Corentin Lauverjat
        ltyp_to_ttyp (v.Lustrec.Lustre_types.var_type)
273 f0195e96 ploc
      in
274
      Ast.VarSet.add (v.var_id, typ) accu)
275
    Ast.VarSet.empty
276 9b0432bc Corentin Lauverjat
    (Lustrec.Machine_code_common.machine_vars m ) in 
277
    (* adding a dummy variable for printing functions *)
278
    Ast.VarSet.add ("_ignore", BoolT) var_set
279
280
    
281
let machine_to_tiny_encoding bounds_input m = (
282
  let read_vars = read_vars bounds_input m.Lustrec.Machine_code_types.mstep.step_inputs in
283
  Log.report ~level:5 (fun fmt -> fprintf fmt ".. raw machine code %s@ " (show_machine_t m));
284
  let ast_loop_first = machine_body_to_ast true m in
285
  let ast_loop_run = machine_body_to_ast false m in
286
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
287
  let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
288
  {
289
    ast= Ast.Seq (gen_loc (), read_vars, (Ast.Seq (gen_loc (), ast_loop_first, loop)));
290
    variables= machine_to_env m;
291
    location_beg_while = Ast.loc_of_stm ast_loop_body;
292
  }
293
)
294