Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / tiny / tiny_utils.ml @ f0195e96

History | View | Annotate | Download (6.76 KB)

1

    
2
module Ast = Tiny.Ast
3

    
4

    
5
let lloc_to_tloc loc = Tiny.Location.dummy (*TODO*)
6
                     
7
let tloc_to_lloc loc = Location.dummy_loc (*TODO*)
8

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

    
16
let cst_bool loc b =
17
  { Ast.expr_desc =
18
      if b then
19
        Ast.Cst(Q.of_int 1, "true")
20
      else
21
        Ast.Cst(Q.of_int 0, "false");
22
    expr_loc = loc;
23
    expr_type = Ast.BoolT }
24
  
25
let rec real_to_q man exp =
26
  if exp = 0 then
27
        Q.of_string (Num.string_of_num man)
28
  else
29
    if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
30
    else (* if exp<0 then *)
31
      Q.mul
32
        (real_to_q man (exp+1))
33
        (Q.of_int 10)
34

    
35
let instr_loc i =
36
  match i.Machine_code_types.lustre_eq with
37
  | None -> Tiny.Location.dummy
38
  | Some eq -> lloc_to_tloc eq.eq_loc
39
             
40
let rec lval_to_texpr loc _val =
41
  let build d v =
42
      Ast.{ expr_desc = d;
43
            expr_loc = loc;
44
            expr_type = v }
45
  in
46
  let new_desc =
47
    match _val.Machine_code_types.value_desc with
48
  | Machine_code_types.Cst cst -> (
49
    match cst with
50
      Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
51
    | Const_real r -> Ast.Cst (Real.to_q r, Real.to_string r) 
52
      | _ -> assert false
53
  )
54
     
55
  | Var v -> Ast.Var (v.var_id)
56
  | Fun (op, vl) ->
57
     let t_arg = match vl with
58
       | hd::_ -> ltyp_to_ttyp hd.value_type
59
       | _ -> assert false
60
     in
61
     (
62
       match op, List.map (lval_to_texpr loc) vl with
63
       | "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2)
64
       | "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2)
65
       | "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2)
66
       | "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2)
67
       | "<", [v1;v2] ->
68
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
69
       | "<=", [v1;v2] ->
70
          Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
71
       | ">", [v1;v2] ->
72
          Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
73
       | ">=", [v1;v2] ->
74
          Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
75
       | "=", [v1;v2] ->
76
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
77
       | "!=", [v1;v2] ->
78
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
79
       | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
80
  )
81
  | _ -> assert false (* no array. access or power *)
82
  in
83
  build new_desc (ltyp_to_ttyp _val.value_type)
84

    
85
  
86
let machine_body_to_ast init m =
87
  let init_var = ref None in
88
  let rec guarded_expr_to_stm loc te guarded_instrs =
89
    match guarded_instrs with
90
    | [] -> assert false
91
    | [_,il] -> instrl_to_stm il
92
    | (label, il)::tl ->
93
       let stmt = instrl_to_stm il in
94
       let guard= match label with
95
           "true" -> te
96
         | "false" -> Ast.neg_guard te
97
         | _ -> assert false (* TODO: don't deal with non boolean
98
                                guards. Could just treturn true and
99
                                over-approximate behavior *)
100
       in
101
       if (match !init_var, te.Ast.expr_desc with
102
           | Some v, Var v2 -> v = v2
103
           | _ -> false) then 
104
         instrl_to_stm (
105
             if init then
106
               (List.assoc "true" guarded_instrs)
107
             else
108
               (List.assoc "false" guarded_instrs)
109
           )
110
       else
111
         Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl)
112
  and instr_to_stm i =
113
    let loc = instr_loc i in
114
    match i.instr_desc with
115
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
116
       Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
117
    | MBranch (e, guarded_instrs) -> (
118
      let te = lval_to_texpr loc e in
119
      guarded_expr_to_stm loc te guarded_instrs
120
    )
121
    | MStep (ol, id, args) ->
122
       if List.mem_assoc id m.Machine_code_types.minstances then
123
         let fun_name, _ = List.assoc id m.minstances in
124
         match Corelang.node_name fun_name, ol with
125
         | "_arrow", [o] -> (
126
           init_var := Some o.var_id;
127
           Ast.Nop (loc);
128
             (* Ast.Asn (loc, o.var_id, 
129
              *        { expr_desc =              if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false");
130
              *          expr_loc = loc;
131
              *          expr_type = Ast.BoolT }
132
              * ) *)
133
         )
134
         | name, _ -> 
135
            (
136
              Format.eprintf "No tiny translation for node call  %s@.@?" name;
137
              assert false
138
            )
139
       else (
140
         Format.eprintf "No tiny translation for node call  %s@.@?" id;
141
         assert false
142
       )
143
    | MReset id
144
      | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
145
    | MComment s 
146
      | MSpec s -> assert false
147
  and instrl_to_stm il =
148
    match il with
149
      [] -> assert false
150
    | [i] -> instr_to_stm i
151
    | i::il ->
152
       let i' = instr_to_stm i in
153
       Ast.Seq (instr_loc i, i', (instrl_to_stm il))
154
  in
155
  instrl_to_stm m.Machine_code_types.mstep.step_instrs 
156

    
157
let read_var loc bounds_opt v =
158
  let min, max =
159
    match bounds_opt with
160
      Some (min,max) -> min, max
161
    | None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
162
  in
163
  let range = {
164
      Ast.expr_desc = Ast.Rand (min,max);
165
      expr_loc = loc;
166
      expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
167
    }
168
  in
169
  Ast.Asn (loc, v.var_id, range)
170
  
171
let rec read_vars loc bounds_inputs vl =
172
  match vl with
173
    [] -> Ast.Nop loc
174
  | [v] -> read_var
175
             loc
176
             (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
177
                Some (List.assoc v.Lustre_types.var_id bounds_inputs)
178
              else
179
                None)
180
             v
181
  | v::tl ->
182
     Ast.Seq (loc,
183
              read_var
184
                loc
185
                (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
186
                   Some (List.assoc v.Lustre_types.var_id bounds_inputs)
187
                 else
188
                   None)
189
                v,
190
              read_vars loc bounds_inputs tl
191
       )
192
  
193
let machine_to_ast bounds_input m =
194
  let loc = Tiny.Location.dummy in
195
  let read_vars = read_vars loc bounds_input m.Machine_code_types.mstep.step_inputs in
196
  let ast_loop_first = machine_body_to_ast true m in
197
  let ast_loop_run = machine_body_to_ast false m in
198
  let ast_loop_body = Ast.Seq (loc, read_vars, ast_loop_run) in
199
  let loop = Ast.While(loc, cst_bool loc true, ast_loop_body) in
200
  Ast.Seq (loc, read_vars, (Ast.Seq (loc, ast_loop_first, loop)))
201
  
202
let machine_to_env m =
203
  
204
    List.fold_left (fun accu v ->
205
      let typ =
206
        ltyp_to_ttyp (v.Lustre_types.var_type)
207
      in
208
      Ast.VarSet.add (v.var_id, typ) accu)
209
    Ast.VarSet.empty
210
    (Machine_code_common.machine_vars m)
211