Project

General

Profile

« Previous | Next » 

Revision 7d62bf41

Added by Pierre-Loïc Garoche almost 5 years ago

Merged code

View differences:

Makefile.in
72 72
	mkdir -p ${datadir}
73 73
	install -m 0655 share/FindLustre.cmake ${datadir}
74 74

  
75
.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
75
.PHONY: $(LOCAL_BINDIR)/lustrec compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
76 76

  
src/Makefile
1
OCAMLBUILD=/home/ploc/.opam/4.03.0+trunk/bin/ocamlbuild -classic-display -use-ocamlfind -no-links 
2

  
3
prefix=/home/ploc/Local
4
exec_prefix=${prefix}
5
bindir=${exec_prefix}/bin
6
datarootdir = ${prefix}/share
7
includedir = ${prefix}/include
8

  
9
LUSI_LIBS=include/math.lusi include/conv.lusi
10
LOCAL_BINDIR=../bin
11
LOCAL_DOCDIR=../doc/manual
12

  
13
lustrec:
14
	@echo Compiling binary lustrec
15
	@$(OCAMLBUILD) main_lustre_compiler.native
16
	@mkdir -p $(LOCAL_BINDIR)
17
	@mv _build/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
18

  
19
doc:
20
	@echo Generating doc
21
	@$(OCAMLBUILD) lustrec.docdir/index.html
22
	@rm -rf $(LOCAL_DOCDIR)
23
	@cp -rf _build/lustrec.docdir $(LOCAL_DOCDIR)
24

  
25
dot: doc
26
	$(OCAMLBUILD) lustrec.docdir/lustrec.dot
27
	dot -T ps -o lustrec.dot _build/lustrec.docdir/lustrec.dot
28
	mv _build/lustrec.docdir/lustrec.dot $(LOCAL_DOCDIR)
29

  
30
clean:
31
	$(OCAMLBUILD) -clean
32

  
33
dist-clean: clean
34
	rm -f Makefile myocamlbuild.ml config.log config.status configure
35
	rm -f include/*.lusic include/math.h include/conv.h
36

  
37
install:
38
	make -C .. install
39

  
40
.PHONY: compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean
41

  
src/_tags
1
"backends": include
1 2
"backends/C": include
2 3
"backends/Horn": include
3 4
"backends/EMF": include
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 77
    
94 78
let pp_stmt fmt stmt =
95 79
  match stmt with
......
125 109
  | Open _ 
126 110
  | TypeDef _ -> eprintf "should not happen in EMF backend"
127 111

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

  
129
let translate fmt prog =
146

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

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

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

  
src/machine_code.ml
78 78
  mannot: expr_annot list;
79 79
}
80 80

  
81
let get_node_def id m =
82
  try
83
    let (decl, _) = List.assoc id m.minstances in
84
    Corelang.node_of_top decl
85
  with Not_found -> raise Not_found
86
    
81 87
let pp_step fmt s =
82 88
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
83 89
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
......
562 568
	   backends. *)
563 569
	(*match !Options.output with
564 570
	| "horn" -> s
565
	| "C" | "java" | _ ->*) join_guards_list s
571
	  | "C" | "java" | _ ->*)
572
	if !Backends.join_guards then
573
	  join_guards_list s
574
	else
575
	  s
566 576
      );
567 577
      step_asserts =
568 578
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
......
579 589
  List.map
580 590
    (fun decl ->
581 591
     let node = node_of_top decl in
582
      let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in
592
      let sch = (Scheduling.get_node_schedule node node_schs).Scheduling.schedule in
583 593
      translate_decl node sch
584 594
    ) nodes
585 595

  
src/main_lustre_compiler.ml
90 90

  
91 91
let functional_backend () = 
92 92
  match !Options.output with
93
  | "horn" | "lustre" | "emf" | "acsl" -> true
93
  | "horn" | "lustre" | "acsl" -> true
94 94
  | _ -> false
95 95

  
96 96
let dynamic_checks () =
......
389 389
       let source_file = destname ^ ".emf" in (* Could be changed *)
390 390
       let source_out = open_out source_file in
391 391
       let fmt = formatter_of_out_channel source_out in
392
       EMF_backend.translate fmt prog;
392
       EMF_backend.translate fmt prog machine_code;
393 393
       ()
394 394
     end
395 395

  
src/optimize_machine.ml
258 258

  
259 259
let machines_unfold consts node_schs machines =
260 260
  List.fold_right (fun m (machines, removed) ->
261
    let fanin = (IMap.find m.mname.node_id node_schs).Scheduling.fanin_table in
261
    let fanin = (Scheduling.get_node_schedule m.mname node_schs).Scheduling.fanin_table in
262 262
    let elim_consts, _ = instrs_unfold fanin IMap.empty (List.map instr_of_const consts) in
263 263
    let (m, removed_m) =  machine_unfold fanin elim_consts m in
264 264
    (m::machines, IMap.add m.mname.node_id removed_m removed)
src/options.ml
44 44
let const_unfold = ref false
45 45
let mpfr = ref false
46 46
let mpfr_prec = ref 0
47

  
47
  
48 48
let traces = ref false
49 49
let horn_cex = ref false
50 50
let horn_query = ref true
......
53 53

  
54 54
let sfunction = ref ""
55 55

  
56

  
56 57
let set_mpfr prec =
57 58
  if prec > 0 then (
58 59
    mpfr := true;
......
61 62
  )
62 63
  else
63 64
    failwith "mpfr requires a positive integer"
64
			
65

  
66
let set_backend s =
67
  output := "emf";
68
  Backends.setup s
69
  
65 70
let options =
66 71
[ "-d", Arg.Set_string dest_dir,
67 72
"uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
......
77 82
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
78 83
    "-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";
79 84
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
80
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
81
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
82
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
83
    "-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
85
    "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
86
    "-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
87
    "-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
88
    "-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
84 89
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
85 90
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
86
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
87
    "-emf", Arg.Unit (fun () -> output := "emf"), "generates EMF output, to be used by CocoSim";
91
    "-lustre", Arg.Unit (fun () -> set_backend "lustre"), "generates Lustre output, performing all active optimizations";
92
    "-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim";
88 93
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
89 94
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
90 95
    "-print_types", Arg.Set print_types, "prints node types";
src/scheduling.ml
15 15
open Graph
16 16
open Causality
17 17

  
18
type eq_schedule_t = ident list list
19
  
18 20
type schedule_report =
19 21
{
20 22
  (* the scheduled node *)
21 23
  node : node_desc;
22 24
  (* a schedule computed wrt the dependency graph *)
23
  schedule : ident list list;
25
  schedule : eq_schedule_t;
24 26
  (* the set of unused variables (no output or mem depends on them) *)
25 27
  unused_vars : ISet.t;
26 28
  (* the table mapping each local var to its in-degree *)
......
31 33
  (*reuse_table : (ident, var_decl) Hashtbl.t*)
32 34
}
33 35

  
36
type t = schedule_report IMap.t
37

  
38
let get_node_schedule node node_schs = Utils.IMap.find node.node_id node_schs
39

  
40
let fold_eq_schedule = List.fold_left
41
  
34 42
(* Topological sort with a priority for variables belonging in the same equation lhs.
35 43
   For variables still unrelated, standard compare is used to choose the minimal element.
36 44
   This priority is used since it helps a lot in factorizing generated code.

Also available in: Unified diff