Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / tiny / tiny_utils.ml @ 25537a17

History | View | Annotate | Download (9.49 KB)

1

    
2
module Ast = Tiny.Ast
3

    
4
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

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

    
17
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");
23
    expr_loc = loc;
24
    expr_type = Ast.BoolT }
25

    
26
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
  
32
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)
41

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

    
47

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

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

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

    
106

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

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

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

    
219
let read_var bounds_opt v =
220
  let min, max =
221
    match bounds_opt with
222
      Some (min,max) -> min, max
223
    | None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
224
  in
225
  let range = {
226
      Ast.expr_desc = Ast.Rand (min,max);
227
      expr_loc = gen_loc ();
228
      expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
229
    }
230
  in
231
  Ast.Asn (gen_loc (), v.var_id, range)
232
  
233
let rec read_vars bounds_inputs vl =
234
  match vl with
235
    [] -> Ast.Nop (gen_loc ())
236
  | [v] -> read_var
237
             (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
238
                Some (List.assoc v.Lustre_types.var_id bounds_inputs)
239
              else
240
                None)
241
             v
242
  | v::tl ->
243
     Ast.Seq (gen_loc (),
244
              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
              read_vars bounds_inputs tl
251
       )
252
  
253
let machine_to_ast bounds_input m =
254
  let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in
255
  (* let ast_init = machine_init_to_ast m in *)
256
  let ast_loop_first = machine_body_to_ast true m in
257
  let ast_loop_run = machine_body_to_ast false m in
258
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
259
  let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
260
  (* Ast.Seq (gen_loc(),
261
   *          ast_init, *)
262
           Ast.Seq (gen_loc (), read_vars,
263
                    Ast.Seq (gen_loc (),
264
                             ast_loop_first,
265
                             loop))
266
         (* ) *)
267
  
268
let machine_to_env m =
269
  List.fold_left (fun accu v ->
270
      Format.eprintf "Adding variable %a to env@." Printers.pp_var v;
271
      let typ =
272
        ltyp_to_ttyp (v.Lustre_types.var_type)
273
      in
274
      Ast.VarSet.add (v.var_id, typ) accu)
275
    Ast.VarSet.empty
276
    (Machine_code_common.machine_vars m)
277