Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Riny / riny_backend.ml @ 3d04f75e

History | View | Annotate | Download (6.45 KB)

1
open LustreSpec
2
open Corelang
3
open Machine_code
4

    
5

    
6
let pp_var fmt id = Format.pp_print_string fmt id.var_id
7

    
8
let rec pp_c_val self pp_var fmt v =
9
  match v with
10
  | Cst c         -> C_backend_common.pp_c_const fmt c
11
  | Array _      
12
  | Access _
13
  | Power _  -> assert false
14
  | LocalVar v    -> pp_var fmt v
15
  | StateVar v    ->
16
    (* array memory vars are represented by an indirection to a local var with the right type,
17
       in order to avoid casting everywhere. *)
18
    if Types.is_array_type v.var_type
19
    then assert false
20
    else Format.fprintf fmt "%s_%a" self pp_var v
21
  | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
22

    
23
module CSrc = C_backend_src.Main (C_backend_src.EmptyMod) 
24
(* let pp_assign = CSrc.pp_assign *)
25
    
26
let pp_assign m self pp_var fmt var_type var_name value =
27
  Format.fprintf fmt "%a = %a;" 
28
    (pp_c_val self pp_var) var_name
29
    (pp_c_val self pp_var) value
30

    
31

    
32
let check_type_restrictions m =
33
  (* Checking that all memories are of type real. Since everything should be
34
     inlined, only arrows instances would be allowed *)
35
  let is_real_var v = Types.is_real_type v.var_type in
36
  if not (List.for_all is_real_var m.mmemory) then (
37
    Format.eprintf "Main node contains variable with non real type: %s@.@?"
38
      (List.find (fun v -> not (is_real_var v)) m.mmemory).var_id ;
39
    assert false
40
  ) else
41
    Format.printf " - All variables are real: OK@.";
42

    
43
    
44
  let call_name (_, (td, _)) = node_name td in 
45
  let is_arrow_call c = call_name c = "_arrow" in
46
  if not (List.for_all is_arrow_call m.minstances) then (
47
    Format.eprintf "All calls are not inlined: call to node %s@.@?"
48
      (call_name (List.find (fun c -> not (is_arrow_call c)) m.minstances)) ;
49
    assert false    
50
  ) else
51
    Format.printf " - All calls inlined: OK@."
52

    
53
    
54

    
55
let rec pp_conditional (m: machine_t) self fmt c tl el =
56
  Format.fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
57
    (pp_c_val self pp_var) c
58
    (Utils.pp_newline_if_non_empty tl)
59
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) tl
60
    (Utils.pp_newline_if_non_empty el)
61
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr m self)) el
62

    
63
and pp_machine_instr (m: machine_t) self fmt instr =
64
  match instr with 
65
  | MReset i -> assert false (* no reset allowed *)
66
  | MLocalAssign (i,v) -> 
67
    pp_assign m self pp_var fmt i.var_type (LocalVar i) v
68
  | MStateAssign (i,v) (* state variable are handled as local ones *)
69
    -> pp_assign m self pp_var fmt i.var_type (StateVar i) v
70
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
71
    pp_machine_instr m self fmt (MLocalAssign (i0, Fun (i, vl)))
72
  | MStep (il, i, vl) -> 
73
    assert false (* no calls *)
74
  | MBranch (g,hl) -> 
75
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
76
    then (* boolean case, needs special treatment in C because truth value is not unique *)
77
	 (* may disappear if we optimize code by replacing last branch test with default *)
78
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
79
      let el = try List.assoc tag_false hl with Not_found -> [] in
80
      pp_conditional m self fmt g tl el
81
    else (* enum type case *)
82
      assert false
83

    
84
let rec extract_init_step m instrs = 
85
  let extract = extract_init_step m in
86
    let f instr = 
87
      match instr with
88
      | MReset i -> assert false (* no reset allowed *)
89
      | MLocalAssign _ 
90
      | MStateAssign _ -> instr, instr
91
      | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
92
	let instr = MLocalAssign (i0, Fun (i, vl)) in
93
	instr, instr
94
      | MStep (il, i, vl) -> (
95
	let (n,_) = List.assoc i m.minstances in
96
	match node_name n, vl, il with
97
	| "_arrow", [i1; i2], [o] -> 
98
	  MLocalAssign(o, i1), MLocalAssign(o, i2) 
99
	| _ -> assert false (* no calls allowed *)
100
      )
101
      
102
    | MBranch (g,hl) -> 
103
      if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
104
      then 
105
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
106
      let el = try List.assoc tag_false hl with Not_found -> [] in
107
      let tl_init, tl_step = extract tl in
108
      let el_init, el_step = extract el in
109
	MBranch(g, [tag_true, tl_init; tag_false, el_init]),
110
	MBranch(g, [tag_true, el_init; tag_false, el_step])
111
      else (* enum type case *)
112
	assert false
113
  in
114
  List.fold_right 
115
    (fun i (init, step) -> let i_i, i_s = f i in i_i::init, i_s::step) 
116
    instrs
117
    ([], [])
118

    
119
let rec filter_bool_assigns instrs =
120
  let filter_instr instr res =
121
    match instr with
122
      | MReset i -> assert false (* no reset allowed *)
123
      | MLocalAssign (i,v) when not (Types.is_real_type i.var_type) -> res
124
      | MLocalAssign _ 
125
      | MStateAssign _ -> instr::res
126
      | MStep _ -> instr::res      
127
      | MBranch (g,hl) -> MBranch(g, List.map (fun (t,il) -> t, filter_bool_assigns il) hl)::res
128
  in
129
  List.fold_right filter_instr instrs []
130

    
131
let pp_randomized_input fmt v = 
132
  Format.fprintf fmt "%s = rand(-1, 1);" v.var_id
133
 
134
let translate fmt basename normalized_prog machines =
135
  (* No modular compilation: require a main node *)
136
  let main_node =
137
    match !Options.main_node with
138
    | "" ->  failwith "Main node required for riny backend" 
139
    | main_node -> (
140
      match Machine_code.get_machine_opt main_node machines with
141
      | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; assert false
142
      | Some m -> m
143
    )
144
  in
145

    
146
  (* Verify that we have only real variables (no bool nor int) *)
147
  check_type_restrictions main_node;
148
  
149
  (* Project instrs to init and step versions *)
150
  let init, step = extract_init_step main_node main_node.mstep.step_instrs in
151
  let init = Optimize_machine.instrs_fusion init in
152
  let step = Optimize_machine.instrs_fusion step in
153
  (* Removing bool assigns that remain from _arrow *)
154
  let init = filter_bool_assigns init in
155
  let step = filter_bool_assigns step in
156
  (* Print the step instructions with all arrows to true *)
157
  Format.fprintf fmt "@[<v 0>%a@ @[<v 2>while (0. < 1.) {@ %a@ %a@]@ }@ @]@."
158
    (* Printing first loop body *)
159
    (Utils.fprintf_list ~sep:"@ "
160
       (pp_machine_instr main_node main_node.mname.node_id))
161
    init
162
    (* Randomized inputs *)
163
    (Utils.fprintf_list ~sep:"@ "
164
       pp_randomized_input)
165
       main_node.mstep.step_inputs
166
    (* Loop body *)
167
    (Utils.fprintf_list ~sep:"@ "
168
       (pp_machine_instr main_node main_node.mname.node_id))
169
    step;
170
  (* Print only the main node (should have been inlined) *)
171
  
172
  (* Each input is declared as a in = rand(min, max); *)
173

    
174

    
175
  ()
176

    
177
(* Local Variables: *)
178
(* compile-command:"make -C ../../.." *)
179
(* End: *)