Project

General

Profile

Download (6.77 KB) Statistics
| Branch: | Tag: | Revision:
1
module Ast = Tiny.Ast
2

    
3
let gen_loc () = Tiny.Location.dummy ()
4

    
5
let lloc_to_tloc loc =
6
  Tiny.Location.location_of_positions loc.Location.loc_start
7
    loc.Location.loc_end
8

    
9
let tloc_to_lloc loc = assert false
10
(*Location.dummy_loc (*TODO*) *)
11

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

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

    
28
let cst_num loc t q =
29
  { Ast.expr_desc = Ast.Cst (q, Q.to_string q); expr_loc = loc; expr_type = t }
30

    
31
let rec real_to_q man exp =
32
  if exp = 0 then Q.of_string (Num.string_of_num man)
33
  else if exp > 0 then Q.div (real_to_q man (exp - 1)) (Q.of_int 10)
34
  else (* if exp<0 then *)
35
    Q.mul (real_to_q man (exp + 1)) (Q.of_int 10)
36

    
37
let instr_loc i =
38
  match i.Machine_code_types.lustre_eq with
39
  | None ->
40
    gen_loc ()
41
  | Some eq ->
42
    lloc_to_tloc eq.eq_loc
43

    
44
let rec lval_to_texpr loc _val =
45
  let build d v = Ast.{ expr_desc = d; expr_loc = gen_loc (); expr_type = v } 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 ->
51
        Ast.Cst (Q.of_int n, string_of_int n)
52
      | Const_real r ->
53
        Ast.Cst (Real.to_q r, Real.to_string r)
54
      | _ ->
55
        assert false)
56
    | Var v ->
57
      Ast.Var v.var_id
58
    | Fun (op, vl) -> (
59
      let t_arg =
60
        match vl with
61
        | hd :: _ ->
62
          ltyp_to_ttyp hd.value_type
63
        | _ ->
64
          assert false
65
      in
66
      match op, List.map (lval_to_texpr loc) vl with
67
      | "+", [ v1; v2 ] ->
68
        Ast.Binop (Ast.Plus, v1, v2)
69
      | "-", [ v1; v2 ] ->
70
        Ast.Binop (Ast.Minus, v1, v2)
71
      | "*", [ v1; v2 ] ->
72
        Ast.Binop (Ast.Times, v1, v2)
73
      | "/", [ v1; v2 ] ->
74
        Ast.Binop (Ast.Div, v1, v2)
75
      | "<", [ v1; v2 ] ->
76
        Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
77
      | "<=", [ v1; v2 ] ->
78
        Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
79
      | ">", [ v1; v2 ] ->
80
        Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
81
      | ">=", [ v1; v2 ] ->
82
        Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
83
      | "=", [ v1; v2 ] ->
84
        Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
85
      | "!=", [ v1; v2 ] ->
86
        Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
87
      | "uminus", [ v1 ] ->
88
        Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1)
89
      | _ ->
90
        Format.eprintf "No tiny translation for operator %s@.@?" op;
91
        assert false)
92
    | _ ->
93
      assert false
94
    (* no array. access or power *)
95
  in
96
  build new_desc (ltyp_to_ttyp _val.value_type)
97

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

    
170
let read_var bounds_opt v =
171
  let min, max =
172
    match bounds_opt with
173
    | Some (min, max) ->
174
      min, max
175
    | None ->
176
      (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
177
  in
178
  let range =
179
    {
180
      Ast.expr_desc = Ast.Rand (min, max);
181
      expr_loc = gen_loc ();
182
      expr_type = ltyp_to_ttyp v.Lustre_types.var_type;
183
    }
184
  in
185
  Ast.Asn (gen_loc (), v.var_id, range)
186

    
187
let rec read_vars bounds_inputs vl =
188
  match vl with
189
  | [] ->
190
    Ast.Nop (gen_loc ())
191
  | [ v ] ->
192
    read_var
193
      (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
194
       Some (List.assoc v.Lustre_types.var_id bounds_inputs)
195
      else None)
196
      v
197
  | v :: tl ->
198
    Ast.Seq
199
      ( gen_loc (),
200
        read_var
201
          (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
202
           Some (List.assoc v.Lustre_types.var_id bounds_inputs)
203
          else None)
204
          v,
205
        read_vars bounds_inputs tl )
206

    
207
let machine_to_ast bounds_input m =
208
  let read_vars =
209
    read_vars bounds_input m.Machine_code_types.mstep.step_inputs
210
  in
211
  let ast_loop_first = machine_body_to_ast true m in
212
  let ast_loop_run = machine_body_to_ast false m in
213
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
214
  let loop =
215
    Ast.While (gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body)
216
  in
217
  Ast.Seq (gen_loc (), read_vars, Ast.Seq (gen_loc (), ast_loop_first, loop))
218

    
219
let machine_to_env m =
220
  List.fold_left
221
    (fun accu v ->
222
      let typ = ltyp_to_ttyp v.Lustre_types.var_type in
223
      Ast.VarSet.add (v.var_id, typ) accu)
224
    Ast.VarSet.empty
225
    (Machine_code_common.machine_vars m)
(2-2/3)