Project

General

Profile

Revision 25537a17 src/tools/tiny/tiny_utils.ml

View differences:

src/tools/tiny/tiny_utils.ml
43 43
  match i.Machine_code_types.lustre_eq with
44 44
  | None -> gen_loc ()
45 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
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
53 59
  let new_desc =
54 60
    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 *)
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 *)
90 103
  in
91 104
  build new_desc (ltyp_to_ttyp _val.value_type)
92 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
93 142
  
94 143
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 =
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 =
97 153
    match guarded_instrs with
98 154
    | [] -> assert false
99 155
    | [_,il] -> instrl_to_stm il
......
106 162
                                guards. Could just treturn true and
107 163
                                over-approximate behavior *)
108 164
       in
109
       if (match !init_var, te.Ast.expr_desc with
110
           | Some v, Var v2 -> v = v2
111
           | _ -> false) then 
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 
112 168
         instrl_to_stm (
113 169
             if init then
114 170
               (List.assoc "true" guarded_instrs)
......
121 177
    let loc = instr_loc i in
122 178
    match i.instr_desc with
123 179
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
124
       Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
180
       Ast.Asn (loc, v.var_id, (lval_to_texpr m loc) e)
125 181
    | MBranch (e, guarded_instrs) -> (
126
      let te = lval_to_texpr loc e in
182
      let te = lval_to_texpr m loc e in
127 183
      guarded_expr_to_stm loc te guarded_instrs
128 184
    )
129 185
    | MStep (ol, id, args) ->
......
131 187
         let fun_name, _ = List.assoc id m.minstances in
132 188
         match Corelang.node_name fun_name, ol with
133 189
         | "_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
              * ) *)
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
          * ) *)
141 202
         )
142 203
         | name, _ -> 
143 204
            (
......
152 213
      | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
153 214
    | MComment s 
154 215
      | 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 216
  in
163 217
  instrl_to_stm m.Machine_code_types.mstep.step_instrs 
164 218

  
......
198 252
  
199 253
let machine_to_ast bounds_input m =
200 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 *)
201 256
  let ast_loop_first = machine_body_to_ast true m in
202 257
  let ast_loop_run = machine_body_to_ast false m in
203 258
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
204 259
  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)))
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
         (* ) *)
206 267
  
207 268
let machine_to_env m =
208
  
209
    List.fold_left (fun accu v ->
269
  List.fold_left (fun accu v ->
270
      Format.eprintf "Adding variable %a to env@." Printers.pp_var v;
210 271
      let typ =
211 272
        ltyp_to_ttyp (v.Lustre_types.var_type)
212 273
      in

Also available in: Unified diff