Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / tiny / tiny_utils.ml @ 820616b1

History | View | Annotate | Download (9.66 KB)

1
let report = Log.report ~plugin:"tiny"
2

    
3
           
4
module Ast = Tiny.Ast
5

    
6
let gen_loc () = Tiny.Location.dummy ()
7
               
8
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Location.loc_start loc.Location.loc_end
9
                     
10
let tloc_to_lloc loc = assert false (*Location.dummy_loc (*TODO*) *)
11

    
12
                     
13
let ltyp_to_ttyp t =
14
  if Types.is_real_type t then Tiny.Ast.RealT
15
  else if Types.is_int_type t then Tiny.Ast.IntT
16
  else if Types.is_bool_type t then Tiny.Ast.BoolT
17
  else assert false (* not covered yet *)
18

    
19
let cst_bool loc b =
20
  { Ast.expr_desc =
21
      if b then
22
        Ast.Cst(Q.of_int 1, "true")
23
      else
24
        Ast.Cst(Q.of_int 0, "false");
25
    expr_loc = loc;
26
    expr_type = Ast.BoolT }
27

    
28
let cst_num loc t q =
29
{ Ast.expr_desc =
30
    Ast.Cst(q, Q.to_string q);
31
  expr_loc = loc;
32
  expr_type = t }
33
  
34
let rec real_to_q man exp =
35
  if exp = 0 then
36
        Q.of_string (Num.string_of_num man)
37
  else
38
    if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
39
    else (* if exp<0 then *)
40
      Q.mul
41
        (real_to_q man (exp+1))
42
        (Q.of_int 10)
43

    
44
let instr_loc i =
45
  match i.Machine_code_types.lustre_eq with
46
  | None -> gen_loc ()
47
  | Some eq -> lloc_to_tloc eq.eq_loc
48

    
49

    
50
let build_instr d v =
51
  Ast.{ expr_desc = d;
52
        expr_loc = gen_loc ();
53
        expr_type = v }
54

    
55
let cst_false =  Ast.Cst (Q.zero, "false") 
56
let cst_true =  Ast.Cst (Q.one, "true")
57

    
58
  
59
let rec lval_to_texpr m loc _val =
60
  let build = build_instr in
61
  let new_desc =
62
    match _val.Machine_code_types.value_desc with
63
    | Machine_code_types.Cst cst -> (
64
      match cst with
65
        Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
66
      | Const_real r -> Ast.Cst (Real.to_q r, Real.to_string r) 
67
      | Const_tag "true" -> cst_true
68
      | Const_tag "false" -> cst_false
69
      | _ -> Format.eprintf "No tiny translation for constant %a@.@?"
70
               (Machine_code_common.pp_val m) _val; assert false
71
    )
72
                                  
73
    | Var v -> Ast.Var (v.var_id)
74
    | Fun (op, vl) ->
75
       let t_arg = match vl with (* t_arg denotes the type of first argument. *)
76
         | hd::_ -> ltyp_to_ttyp hd.value_type
77
         | _ -> assert false
78
       in
79
       (
80
         match op, List.map (lval_to_texpr m loc) vl with
81
         | "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2)
82
         | "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2)
83
         | "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2)
84
         | "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2)
85
         | "<", [v1;v2] ->
86
            Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
87
         | "<=", [v1;v2] ->
88
            Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
89
         | ">", [v1;v2] ->
90
            Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
91
         | ">=", [v1;v2] ->
92
            Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
93
         | "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1)
94
         | "=", [v1;v2] -> Ast.Binop (Ast.Eq, v1, v2)
95
         | "equi", [v1;v2] -> Ast.Binop (Ast.Eq, v1, v2)
96
                            
97
         | "!=", [v1;v2] -> Ast.Unop (Ast.Not, build (Ast.Binop (Ast.Eq, v1, v2)) Ast.BoolT)
98
         | "not", [v1] -> Ast.Unop (Ast.Not, v1)
99
         | "&&", [v1;v2] -> Ast.Binop (Ast.And, v1, v2)
100
         | "||", [v1;v2] -> Ast.Binop (Ast.Or, v1, v2)
101
                          
102
         | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
103
       )
104
    | _ -> assert false (* no array. access or power *)
105
  in
106
  build new_desc (ltyp_to_ttyp _val.value_type)
107

    
108

    
109
                       (*
110
let machine_init_to_ast m =
111
  let build_reset i =
112
    match i.Machine_code_types.instr_desc with
113
    | MReset id ->
114
       
115
    | _ -> Format.eprintf "Init instr: %a@." (Machine_code_common.pp_instr m) i; assert false
116
  in
117
build_seq build_reset m.Machine_code_types.minit
118
                        *)
119

    
120
let rec find_init m il =
121
  List.fold_left (fun res i ->
122
      match res with
123
      | Some _ -> res
124
      | _ -> (
125
        match i.Machine_code_types.instr_desc with
126
        | MLocalAssign _ | MStateAssign _ | MReset _| MNoReset _| MComment _|MSpec _
127
          -> None
128
        | MStep (ol, id, args) ->
129
           if List.mem_assoc id m.Machine_code_types.minstances then
130
             let fun_name, _ = List.assoc id m.minstances in
131
             match Corelang.node_name fun_name, ol with
132
             | "_arrow", [o] -> Some o.var_id
133
             | _ -> None
134
           else
135
             None
136
        | MBranch (_, guarded_expr) ->
137
           List.fold_left (
138
               fun res (_, il') ->
139
               match res with Some _ -> res | None -> find_init m il'
140
             ) res guarded_expr
141
      )
142
    )
143
    None il
144
  
145
let machine_body_to_ast init m =
146
  let init_var = find_init m m.Machine_code_types.mstep.step_instrs in
147
  let rec instrl_to_stm il  = 
148
    match il with
149
      [] -> assert false
150
    | [i] -> instr_to_stm i
151
    | i::il -> Ast.Seq (gen_loc (), instr_to_stm i, instrl_to_stm il)
152

    
153
                           
154
  and guarded_expr_to_stm loc te guarded_instrs =
155
    match guarded_instrs with
156
    | [] -> assert false
157
    | [_,il] -> instrl_to_stm il
158
    | (label, il)::tl ->
159
       let stmt = instrl_to_stm il in
160
       let guard= match label with
161
           "true" -> te
162
         | "false" -> Ast.neg_guard te
163
         | _ -> assert false (* TODO: don't deal with non boolean
164
                                guards. Could just treturn true and
165
                                over-approximate behavior *)
166
       in
167
       if (match init_var, te.Ast.expr_desc with
168
           | Some v, Var v2 ->
169
              (* Format.eprintf "Building init (possibly if %b)@." (v=v2);  *)v = v2
170
           | _ ->
171
              (* Format.eprintf "Building if init def? %b @." (match init_var with None -> false | _ -> true);
172
               *)
173
              false
174
          )
175
       then 
176
         instrl_to_stm (
177
             if init then
178
               (List.assoc "true" guarded_instrs)
179
             else
180
               (List.assoc "false" guarded_instrs)
181
           )
182
       else
183
         Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl)
184
  and instr_to_stm i =
185
    let loc = instr_loc i in
186
    match i.instr_desc with
187
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
188
       Ast.Asn (loc, v.var_id, (lval_to_texpr m loc) e)
189
    | MBranch (e, guarded_instrs) -> (
190
      let te = lval_to_texpr m loc e in
191
      guarded_expr_to_stm loc te guarded_instrs
192
    )
193
    | MStep (ol, id, args) ->
194
       if List.mem_assoc id m.Machine_code_types.minstances then
195
         let fun_name, _ = List.assoc id m.minstances in
196
         match Corelang.node_name fun_name, ol with
197
         | "_arrow", [o] -> (
198
           (* init_var := Some o.var_id; *)
199
           Ast.Asn (loc, o.var_id, build_instr (if init then cst_true else cst_false) Ast.BoolT);
200
         (* We set the arrow to
201
            false: we are not anymore  
202
            in init state *)
203
         (*           Format.eprintf "%a = arrow()@." Printers.pp_var o;*)
204
         (*  Ast.Nop (loc); *)
205
         (* Ast.Asn (loc, o.var_id, 
206
          *        { expr_desc =              if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false");
207
          *          expr_loc = loc;
208
          *          expr_type = Ast.BoolT }
209
          * ) *)
210
         )
211
         | name, _ -> 
212
            (
213
              Format.eprintf "No tiny translation for node call  %s@.@?" name;
214
              assert false
215
            )
216
       else (
217
         Format.eprintf "No tiny translation for node call  %s@.@?" id;
218
         assert false
219
       )
220
    | MReset id
221
      | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
222
    | MComment s 
223
      | MSpec s -> assert false
224
  in
225
  instrl_to_stm m.Machine_code_types.mstep.step_instrs 
226

    
227
let read_var bounds_opt v =
228
  let min, max =
229
    match bounds_opt with
230
      Some (min,max) -> min, max
231
    | None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
232
  in
233
  let range = {
234
      Ast.expr_desc = Ast.Rand (min,max);
235
      expr_loc = gen_loc ();
236
      expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
237
    }
238
  in
239
  Ast.Asn (gen_loc (), v.var_id, range)
240
  
241
let rec read_vars bounds_inputs vl =
242
  match vl with
243
    [] -> Ast.Nop (gen_loc ())
244
  | [v] -> read_var
245
             (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
246
                Some (List.assoc v.Lustre_types.var_id bounds_inputs)
247
              else
248
                None)
249
             v
250
  | v::tl ->
251
     Ast.Seq (gen_loc (),
252
              read_var
253
                (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
254
                   Some (List.assoc v.Lustre_types.var_id bounds_inputs)
255
                 else
256
                   None)
257
                v,
258
              read_vars bounds_inputs tl
259
       )
260
  
261
let machine_to_ast bounds_input m =
262
  let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in
263
  (* let ast_init = machine_init_to_ast m in *)
264
  let ast_loop_first = machine_body_to_ast true m in
265
  let ast_loop_run = machine_body_to_ast false m in
266
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
267
  let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
268
  (* Ast.Seq (gen_loc(),
269
   *          ast_init, *)
270
           Ast.Seq (gen_loc (), read_vars,
271
                    Ast.Seq (gen_loc (),
272
                             ast_loop_first,
273
                             loop))
274
         (* ) *)
275
  
276
let machine_to_env m =
277
  List.fold_left (fun accu v ->
278
      report ~level:3 (fun fmt -> Format.fprintf fmt "Adding variable %a to env@." Printers.pp_var v);
279
      let typ =
280
        ltyp_to_ttyp (v.Lustre_types.var_type)
281
      in
282
      Ast.Var.Set.add (v.var_id, typ) accu)
283
    Ast.Var.Set.empty
284
    (Machine_code_common.machine_vars m)
285