Project

General

Profile

Download (7.22 KB) Statistics
| Branch: | Tag: | Revision:
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.Lustrec.Location.loc_start loc.Lustrec.Location.loc_end
7
                     
8
let tloc_to_lloc loc = assert false (*Lustrec.Location.dummy_loc (*TODO*) *)
9

    
10
                     
11
let ltyp_to_ttyp t =
12
  if Lustrec.Types.is_real_type t then Tiny.Ast.RealT
13
  else if Lustrec.Types.is_int_type t then Tiny.Ast.IntT
14
  else if Lustrec.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.Lustrec.Machine_code_types.lustre_eq with
44
  | None -> gen_loc ()
45
  | Some eq -> lloc_to_tloc eq.eq_loc
46
             
47
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
53
  let new_desc =
54
    match _val.Lustrec.Machine_code_types.value_desc with
55
  | Lustrec.Machine_code_types.Cst cst -> (
56
    match cst with
57
      Lustrec.Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
58
    | Const_real r -> Ast.Cst (Lustrec.Real.to_q r, Lustrec.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 *)
90
  in
91
  build new_desc (ltyp_to_ttyp _val.value_type)
92

    
93
  
94
let machine_body_to_ast init m =
95
  let init_var = ref None in
96
  let rec guarded_expr_to_stm loc te guarded_instrs =
97
    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)
120
  and instr_to_stm i =
121
    let loc = instr_loc i in
122
    match i.instr_desc with
123
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
124
       Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
125
    | MBranch (e, guarded_instrs) -> (
126
      let te = lval_to_texpr loc e in
127
      guarded_expr_to_stm loc te guarded_instrs
128
    )
129
    | MStep (ol, id, args) ->
130
       if List.mem_assoc id m.Lustrec.Machine_code_types.minstances then
131
         let fun_name, _ = List.assoc id m.minstances in
132
         match Lustrec.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
155
  and instrl_to_stm il =
156
    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))
162
  in
163
  instrl_to_stm m.Lustrec.Machine_code_types.mstep.step_instrs 
164

    
165
let read_var bounds_opt v =
166
  let min, max =
167
    match bounds_opt with
168
      Some (min,max) -> min, max
169
    | None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
170
  in
171
  let range = {
172
      Ast.expr_desc = Ast.Rand (min,max);
173
      expr_loc = gen_loc ();
174
      expr_type = ltyp_to_ttyp (v.Lustrec.Lustre_types.var_type)
175
    }
176
  in
177
  Ast.Asn (gen_loc (), v.var_id, range)
178
  
179
let rec read_vars bounds_inputs vl =
180
  match vl with
181
    [] -> Ast.Nop (gen_loc ())
182
  | [v] -> read_var
183
             (if List.mem_assoc v.Lustrec.Lustre_types.var_id bounds_inputs then
184
                Some (List.assoc v.Lustrec.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.Lustrec.Lustre_types.var_id bounds_inputs then
192
                   Some (List.assoc v.Lustrec.Lustre_types.var_id bounds_inputs)
193
                 else
194
                   None)
195
                v,
196
              read_vars bounds_inputs tl
197
       )
198
  
199
let machine_to_ast bounds_input m =
200
  let read_vars = read_vars bounds_input m.Lustrec.Machine_code_types.mstep.step_inputs in
201
  let ast_loop_first = machine_body_to_ast true m in
202
  let ast_loop_run = machine_body_to_ast false m in
203
  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
  
207
let machine_to_env m =
208
  
209
    List.fold_left (fun accu v ->
210
      let typ =
211
        ltyp_to_ttyp (v.Lustrec.Lustre_types.var_type)
212
      in
213
      Ast.VarSet.add (v.var_id, typ) accu)
214
    Ast.VarSet.empty
215
    (Lustrec.Machine_code_common.machine_vars m)
216

    
(2-2/3)