Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/tools/tiny/tiny_utils.ml
1

  
2 1
module Ast = Tiny.Ast
3 2

  
4 3
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 4

  
10
                     
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

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

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

  
26 28
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
  
29
  { Ast.expr_desc = Ast.Cst (q, Q.to_string q); expr_loc = loc; expr_type = t }
30

  
32 31
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)
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)
41 36

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

  
47 44
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
45
  let build d v = Ast.{ expr_desc = d; expr_loc = gen_loc (); expr_type = v } in
53 46
  let new_desc =
54 47
    match _val.Machine_code_types.value_desc with
55
  | Machine_code_types.Cst cst -> (
56
    match cst with
57
      Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
58
    | Const_real r -> Ast.Cst (Real.to_q r, 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 *)
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 *)
90 95
  in
91 96
  build new_desc (ltyp_to_ttyp _val.value_type)
92 97

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

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

  
179 187
let rec read_vars bounds_inputs vl =
180 188
  match vl with
181
    [] -> Ast.Nop (gen_loc ())
182
  | [v] -> read_var
183
             (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
184
                Some (List.assoc v.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.Lustre_types.var_id bounds_inputs then
192
                   Some (List.assoc v.Lustre_types.var_id bounds_inputs)
193
                 else
194
                   None)
195
                v,
196
              read_vars bounds_inputs tl
197
       )
198
  
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

  
199 207
let machine_to_ast bounds_input m =
200
  let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in
208
  let read_vars =
209
    read_vars bounds_input m.Machine_code_types.mstep.step_inputs
210
  in
201 211
  let ast_loop_first = machine_body_to_ast true m in
202 212
  let ast_loop_run = machine_body_to_ast false m in
203 213
  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
  
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

  
207 219
let machine_to_env m =
208
  
209
    List.fold_left (fun accu v ->
210
      let typ =
211
        ltyp_to_ttyp (v.Lustre_types.var_type)
212
      in
220
  List.fold_left
221
    (fun accu v ->
222
      let typ = ltyp_to_ttyp v.Lustre_types.var_type in
213 223
      Ast.VarSet.add (v.var_id, typ) accu)
214 224
    Ast.VarSet.empty
215 225
    (Machine_code_common.machine_vars m)
216

  

Also available in: Unified diff