Project

General

Profile

Revision 3ca27bc7 src/backends/EMF/EMF_backend.ml

View differences:

src/backends/EMF/EMF_backend.ml
1
(* EMF backend *)
2
(* This backup is initially motivated by the need to express Spacer computed
3
   invariants as Matlab Simulink executable evidences.
4

  
5
   Therefore the input language is more restricted. We do not expect fancy
6
   datastructure, complex function calls, etc.
7

  
8
   In case of error, use -node foo -inline to eliminate function calls that are
9
   not seriously handled yet.
10
   
11

  
12
   In terms of algorithm, the process was initially based on printing normalized
13
   code. We now rely on machine code printing. The old code is preserved for
14
   reference.
15
*)
16

  
1 17
open LustreSpec
2 18
open Machine_code
3 19
open Format
4 20
open Utils
5 21

  
6 22
exception Unhandled of string
7
  
23
    
24

  
25
(* Basic printing functions *)
26
    
8 27
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
9 28
let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v
10

  
11 29
let pp_node_args = fprintf_list ~sep:", " pp_var_name
12 30

  
13
(* simple function to extract the element id in the list. Starts from 1. *)
31
    
32
(* Matlab starting counting from 1.
33
   simple function to extract the element id in the list. Starts from 1. *)
14 34
let rec get_idx x l =
15 35
  match l with
16 36
  | hd::tl -> if hd = x then 1 else 1+(get_idx x tl)
17 37
  | [] -> assert false
18
     
38

  
39
(**********************************************)
40
(* Old stuff: printing normalized code as EMF *)     
41
(**********************************************)
42

  
43
(*
19 44
let pp_expr vars fmt expr =
20 45
  let rec pp_expr fmt expr =
21 46
    match expr.expr_desc with
......
107 132
  | Const _
108 133
  | Open _
109 134
  | TypeDef _ -> eprintf "should not happen in EMF backend"
135
*)
136

  
137

  
138
(**********************************************)
139
(*   Printing machine code as EMF             *)
140
(**********************************************)
110 141

  
111 142
let rec pp_val vars fmt v =
112 143
  match v.value_desc with
......
142 173
    | "not", [v] -> fprintf fmt "(~%a)" (pp_val vars) v
143 174
    | _ -> fprintf fmt "%s (%a)" id  (Utils.fprintf_list ~sep:", " (pp_val vars)) vl 
144 175

  
176
     
145 177

  
146 178
     
147 179
let rec pp_instr m vars fmt i =
148
  match i with
180
  match Corelang.get_instr_desc i with
149 181
  | MLocalAssign (var,v) 
150 182
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
151 183
  | MStep ([var], i, vl)  -> (
......
177 209
and pp_instrs m vars fmt il =
178 210
  fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m vars)) il
179 211

  
212

  
180 213
let rec get_instr_var i =
181
  match i with
214
  match Corelang.get_instr_desc i with
182 215
  | MLocalAssign (var,_) 
183 216
  | MStateAssign (var,_) 
184 217
  | MStep ([var], _, _)  -> var 
......
194 227
  | i::_ -> get_instr_var i (* looking for the first instr *)
195 228
  | _ -> assert false
196 229

  
230
  
197 231
let rec  get_val_vars v =
198 232
  match v.value_desc with
199 233
  | Cst c -> Utils.ISet.empty
......
201 235
  | StateVar v -> Utils.ISet.singleton v.var_id
202 236
  | Fun (n, vl) -> List.fold_left (fun res v -> Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl
203 237
  | _ -> assert false (* not available in EMF backend *)
204
  
238

  
205 239
let rec get_instr_vars i =
206
  match i with
240
  match Corelang.get_instr_desc i with
207 241
  | MLocalAssign (_,v)  
208 242
  | MStateAssign (_,v) -> get_val_vars v
209 243
  | MStep ([_], _, vl)  -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
......
219 253
  | MBranch _ (* EMF backend only accept true/false ite *)
220 254
  | MReset _           
221 255
  | MNoReset _
222
  | MComment _ -> assert false (* not  available for EMF output *)
256
  | MComment _ -> failwith "Error in compiling some constructs into EMF. Have you considered -node foo -inline options ?" (* not  available for EMF output *)
223 257
and get_instrs_vars il =
224 258
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i))
225 259
    Utils.ISet.empty
......
229 263
  (* first, we extract the expression and associated variables *)
230 264
  let var = get_instr_var i in
231 265
  let vars = Utils.ISet.elements (get_instr_vars i) in	
232
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
266
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @ \"original_lustre_expr\": [%t]@]}"
233 267
    var.var_id
234 268
    (pp_instr m vars) i
235 269
    (fprintf_list ~sep:", " pp_var_string) vars
236
    
270
    (fun fmt -> ()
271
      (*xxxx
272
      if is expr than print associated lustre eq else empty string
273
	xxx todo
274
      *)
275
    ) 
237 276
     
238 277
let pp_machine fmt m =
239 278
  try
......
250 289
    eprintf "%s@ " msg;
251 290
    eprintf "node skipped - no output generated@ @]@."
252 291
  )
292

  
293
(****************************************************)
294
(* Main function: iterates over node and print them *)
295
(****************************************************)
296
let pp_meta fmt basename =
297
  fprintf fmt "\"meta\": @[<v 0>{@ ";
298
  Utils.fprintf_list ~sep:",@ "
299
    (fun fmt (k, v) -> fprintf fmt "\"%s\": \"%s\"" k v)
300
    fmt
301
    ["compiler-name", (Filename.basename Sys.executable_name);
302
     "compiler-version", Version.number;
303
     "command", (String.concat " " (Array.to_list Sys.argv));
304
     "source_file", basename
305
    ]
306
  ;
307
  fprintf fmt "@ @]},@ "
253 308
    
254
let translate fmt prog machines =
309
let translate fmt basename prog machines =
255 310
  fprintf fmt "@[<v 0>{@ ";
311
  pp_meta fmt basename;
312
  fprintf fmt "\"nodes\": @[<v 0>{@ ";
256 313
  (* fprintf_list ~sep:",@ " pp_decl fmt prog; *)
257 314
  fprintf_list ~sep:",@ " pp_machine fmt machines;
315
  fprintf fmt "@ @]}";
258 316
  fprintf fmt "@ @]}"
317

  
318
(* Local Variables: *)
319
(* compile-command: "make -C ../.." *)
320
(* End: *)

Also available in: Unified diff