Project

General

Profile

Revision f7caf067

View differences:

src/backends/EMF/EMF_backend.ml
1 1
open LustreSpec
2
open Machine_code
2 3
open Format
3 4
open Utils
4 5

  
6
exception Unhandled of string
7
  
5 8
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
6 9
let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v
7 10

  
8 11
let pp_node_args = fprintf_list ~sep:", " pp_var_name
9 12

  
13
(* simple function to extract the element id in the list. Starts from 1. *)
14
let rec get_idx x l =
15
  match l with
16
  | hd::tl -> if hd = x then 1 else 1+(get_idx x tl)
17
  | [] -> assert false
18
     
10 19
let pp_expr vars fmt expr =
11
  (* simple function to extract the element id in the list. Starts from 1. *)
12
  let rec get_idx x l =
13
    match l with
14
    | hd::tl -> if hd = x then 1 else 1+(get_idx x tl)
15
    | [] -> assert false
16
  in
17 20
  let rec pp_expr fmt expr =
18 21
    match expr.expr_desc with
19 22
    | Expr_const c -> Printers.pp_const fmt c
......
71 74
  in
72 75
  pp_expr fmt expr
73 76

  
74
(*
75
let rec translate_expr expr vars =
76
  match expr with
77
    match expr.expr_desc with
78
    | Expr_const _ -> expr, vars
79
    | Expr_ident id -> if List.exists id Format.fprintf fmt "%s" id
80
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
81
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
82
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
83
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
84
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
85
    | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
86
    | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
87
    | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
88
    | Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
89
    | Expr_merge (id, hl) ->
90
      fprintf fmt "merge %s %a" id pp_handlers hl
91
    | Expr_appl (id, e, r) -> pp_app fmt id e r
92
*)
93

  
94 77
let pp_stmt fmt stmt =
95 78
  match stmt with
96 79
  | Eq eq -> (
......
125 108
  | Open _
126 109
  | TypeDef _ -> eprintf "should not happen in EMF backend"
127 110

  
111
let rec pp_val vars fmt v =
112
  match v.value_desc with
113
  | Cst c -> Printers.pp_const fmt c
114
  | LocalVar v
115
  | StateVar v ->
116
     let id = v.var_id in
117
     if List.mem id vars then
118
       Format.fprintf fmt "u(%i)" (get_idx id vars)
119
     else
120
       assert false (* impossible to find element id in var list *)
121
  | Fun (n, vl) -> pp_fun vars n fmt vl
122
  | _ -> assert false (* not available in EMF backend *)
123
and pp_fun vars id fmt vl =
124
  eprintf "print %s with %i args@.@?" id (List.length vl);
125
  match id, vl with
126
    | "+", [v1;v2] -> fprintf fmt "(%a + %a)" (pp_val vars) v1 (pp_val vars) v2
127
    | "uminus", [v] -> fprintf fmt "(- %a)" (pp_val vars) v
128
    | "-", [v1;v2] -> fprintf fmt "(%a - %a)" (pp_val vars) v1 (pp_val vars) v2
129
    | "*",[v1;v2] -> fprintf fmt "(%a * %a)" (pp_val vars) v1 (pp_val vars) v2
130
    | "/", [v1;v2] -> fprintf fmt "(%a / %a)" (pp_val vars) v1 (pp_val vars) v2
131
    | "mod", [v1;v2] -> fprintf fmt "mod (%a, %a)" (pp_val vars) v1 (pp_val vars) v2
132
    | "&&", [v1;v2] -> fprintf fmt "(%a & %a)" (pp_val vars) v1 (pp_val vars) v2
133
    | "||", [v1; v2] -> fprintf fmt "(%a | %a)" (pp_val vars) v1 (pp_val vars) v2
134
    | "xor", [v1; v2] -> fprintf fmt "xor (%a, %a)" (pp_val vars) v1 (pp_val vars) v2
135
    | "impl", [v1; v2] -> fprintf fmt "((~%a) | %a)" (pp_val vars) v1 (pp_val vars) v2
136
    | "<", [v1; v2] -> fprintf fmt "(%a < %a)" (pp_val vars) v1 (pp_val vars) v2
137
    | "<=", [v1; v2] -> fprintf fmt "(%a <= %a)" (pp_val vars) v1 (pp_val vars) v2
138
    | ">", [v1; v2] -> fprintf fmt "(%a > %a)" (pp_val vars) v1 (pp_val vars) v2
139
    | ">=", [v1; v2] -> fprintf fmt "(%a >= %a)" (pp_val vars) v1 (pp_val vars) v2
140
    | "!=", [v1; v2] -> fprintf fmt "(%a != %a)" (pp_val vars) v1 (pp_val vars) v2
141
    | "=", [v1; v2] -> fprintf fmt "(%a = %a)" (pp_val vars) v1 (pp_val vars) v2
142
    | "not", [v] -> fprintf fmt "(~%a)" (pp_val vars) v
143
    | _ -> fprintf fmt "%s (%a)" id  (Utils.fprintf_list ~sep:", " (pp_val vars)) vl 
128 144

  
129
let translate fmt prog =
145

  
146
     
147
let rec pp_instr m vars fmt i =
148
  match i with
149
  | MLocalAssign (var,v) 
150
  | MStateAssign (var,v) -> fprintf fmt "y = %a" (pp_val vars) v
151
  | MStep ([var], i, vl)  -> (
152
    let name = (Machine_code.get_node_def i m).node_id in
153
    match name, vl with
154
      "_arrow", [v1; v2] -> (
155
	match v1.value_desc, v2.value_desc with
156
	| Cst c1, Cst c2 -> if c1 = Corelang.const_of_bool true && c2 = Corelang.const_of_bool false then fprintf fmt "STEP" else assert false (* only handle true -> false *)
157
	| _ -> assert false
158
      )
159
    | _ -> raise (Unhandled ("call to node " ^ name))
160
  )
161
  | MBranch (g,[(tag1,case1);(tag2,case2)])     ->
162
     let then_case, else_case =
163
       if tag1 = Corelang.tag_true then
164
	 case1, case2
165
       else
166
	 case2, case1
167
     in
168
     fprintf fmt "if %a; %a; else %a; end"
169
       (pp_val vars) g
170
       (pp_instrs m vars) then_case
171
       (pp_instrs m vars) else_case
172
  | MStep _ (* only single output for function call *)
173
  | MBranch _ (* EMF backend only accept true/false ite *)
174
  | MReset _           
175
  | MNoReset _
176
  | MComment _ -> assert false (* not  available for EMF output *)
177
and pp_instrs m vars fmt il =
178
  fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m vars)) il
179

  
180
let rec get_instr_var i =
181
  match i with
182
  | MLocalAssign (var,_) 
183
  | MStateAssign (var,_) 
184
  | MStep ([var], _, _)  -> var 
185
  | MBranch (_,[(tag1,case1);(tag2,case2)])     ->
186
     get_instrs_var case1 (* assuming case1 and case2 define the same variable *)
187
  | MStep _ (* only single output for function call *)
188
  | MBranch _ (* EMF backend only accept true/false ite *)
189
  | MReset _           
190
  | MNoReset _
191
  | MComment _ -> assert false (* not  available for EMF output *)
192
and get_instrs_var il =
193
  match il with
194
  | i::_ -> get_instr_var i (* looking for the first instr *)
195
  | _ -> assert false
196

  
197
let rec  get_val_vars v =
198
  match v.value_desc with
199
  | Cst c -> Utils.ISet.empty
200
  | LocalVar v
201
  | StateVar v -> Utils.ISet.singleton v.var_id
202
  | Fun (n, vl) -> List.fold_left (fun res v -> Utils.ISet.union (get_val_vars v) res) Utils.ISet.empty vl
203
  | _ -> assert false (* not available in EMF backend *)
204
  
205
let rec get_instr_vars i =
206
  match i with
207
  | MLocalAssign (_,v)  
208
  | MStateAssign (_,v) -> get_val_vars v
209
  | MStep ([_], _, vl)  -> List.fold_left (fun res v -> Utils.ISet.union res (get_val_vars v)) Utils.ISet.empty vl 
210
  | MBranch (c,[(_,case1);(_,case2)])     ->
211
     Utils.ISet.union
212
       (get_val_vars c)
213
       (
214
	 Utils.ISet.union
215
	   (get_instrs_vars case1)
216
	   (get_instrs_vars case2)
217
       )
218
  | MStep _ (* only single output for function call *)
219
  | MBranch _ (* EMF backend only accept true/false ite *)
220
  | MReset _           
221
  | MNoReset _
222
  | MComment _ -> assert false (* not  available for EMF output *)
223
and get_instrs_vars il =
224
  List.fold_left (fun res i -> Utils.ISet.union res (get_instr_vars i))
225
    Utils.ISet.empty
226
    il
227
    
228
let pp_instr_main m fmt i =
229
  (* first, we extract the expression and associated variables *)
230
  let var = get_instr_var i in
231
  let vars = Utils.ISet.elements (get_instr_vars i) in	
232
  fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\",@ \"vars\": [%a] @]}"
233
    var.var_id
234
    (pp_instr m vars) i
235
    (fprintf_list ~sep:", " pp_var_string) vars
236
    
237
     
238
let pp_machine fmt m =
239
  try
240
    fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a],@ \"outputs\": [%a],@ "
241
      m.mname.node_id
242
      pp_node_args m.mstep.step_inputs
243
      pp_node_args m.mstep.step_outputs;
244
    fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
245
      (fprintf_list ~sep:",@ " (pp_instr_main m)) m.mstep.step_instrs;
246
    fprintf fmt "@]@ }"
247
  with Unhandled msg -> (
248
    eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
249
      m.mname.node_id;
250
    eprintf "%s@ " msg;
251
    eprintf "node skipped - no output generated@ @]@."
252
  )
253
    
254
let translate fmt prog machines =
130 255
  fprintf fmt "@[<v 0>{@ ";
131
  fprintf_list ~sep:",@ " pp_decl fmt prog;
256
  (* fprintf_list ~sep:",@ " pp_decl fmt prog; *)
257
  fprintf_list ~sep:",@ " pp_machine fmt machines;
132 258
  fprintf fmt "@ @]}"
src/machine_code.ml
89 89
  mannot: expr_annot list;
90 90
}
91 91

  
92
(* merge log: get_node_def was in c0f8 *)
93
let get_node_def id m =
94
  try
95
    let (decl, _) = List.assoc id m.minstances in
96
    Corelang.node_of_top decl
97
  with Not_found -> raise Not_found
98
    
99
(* merge log: machine_vars was in 44686 *)
92 100
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
93 101

  
94 102
let pp_step fmt s =
......
616 624
	   backends. *)
617 625
	(*match !Options.output with
618 626
	| "horn" -> s
619
	| "C" | "java" | _ ->*) join_guards_list s
627
	  | "C" | "java" | _ ->*)
628
	if !Backends.join_guards then
629
	  join_guards_list s
630
	else
631
	  s
620 632
      );
621 633
      step_asserts = List.map (translate_expr nd init_args) nd_node_asserts;
622 634
    };
src/main_lustre_compiler.ml
376 376
       let source_file = destname ^ ".emf" in (* Could be changed *)
377 377
       let source_out = open_out source_file in
378 378
       let fmt = formatter_of_out_channel source_out in
379
       EMF_backend.translate fmt prog;
379
       EMF_backend.translate fmt prog machine_code;
380 380
       ()
381 381
     end
382 382

  
src/options.ml
142 142
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
143 143
    "-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
144 144
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
145
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
146
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produces traceability file for Horn backend. Enable the horn backend.";
147
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generates cex enumeration. Enable the horn backend (work in progress)";
148
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generates queries in generated Horn file. Enable the horn backend (work in progress)";
149
    "-horn-sfunction", Arg.Set_string sfunction, "gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
145
    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
146
    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
147
    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
148
    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
149
    "-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m";
150 150
    "-print-reuse", Arg.Set print_reuse, "prints variable reuse policy";
151 151
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
152
   "-emf", Arg.Unit (fun () -> output := "emf"), "generates EMF output, to be used by CocoSim";
152
   "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
153 153
   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
154 154
    "-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation";
155 155
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
156
    "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
157 156
    
158 157
    "-c++" , Arg.Set        cpp      , "c++ backend";
159 158
    "-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")";

Also available in: Unified diff