Project

General

Profile

Revision a6df3992

View differences:

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

  
3 3
prefix=/home/ploc/Local
4 4
exec_prefix=${prefix}
src/_tags
1 1
"backends/C": include
2 2
"backends/Horn": include
3
"backends/EMF": include
3 4
"plugins/scopes": include
4 5
<**/.svn>: -traverse
5 6
<**/.svn>: not_hygienic
src/automata.ml
69 69

  
70 70
let rec unless_read reads handler =
71 71
  let res =
72
  List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_unless
72
  List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_unless
73 73
  in
74 74
(
75 75
(*
......
80 80
)
81 81

  
82 82
let rec until_read reads handler =
83
  List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_until
83
  List.fold_left (fun read (_, c, _, _) -> Utils.ISet.union read (get_expr_vars c)) reads handler.hand_until
84 84

  
85 85
let rec handler_read reads handler =
86 86
  let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
87 87
  let allvars =
88 88
    List.fold_left (fun read stmt ->
89 89
      match stmt with
90
      | Eq eq -> get_expr_vars read eq.eq_rhs
90
      | Eq eq -> Utils.ISet.union read (get_expr_vars eq.eq_rhs)
91 91
      | Aut aut -> automata_read read aut) reads handler.hand_stmts
92 92
  in let res = ISet.diff allvars locals
93 93
     in
src/backends/EMF/EMF_backend.ml
1
open LustreSpec
2
open Format
3
open Utils
4

  
5
let pp_var_string fmt v = fprintf fmt "\"%s\"" v
6
let pp_var_name fmt v = fprintf fmt "\"%a\"" Printers.pp_var_name v
7

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

  
10
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
  let rec pp_expr fmt expr =
18
    match expr.expr_desc with
19
    | Expr_const c -> Printers.pp_const fmt c
20
    | Expr_ident id ->
21
       if List.mem id vars then
22
	 Format.fprintf fmt "u(%i)" (get_idx id vars)
23
       else
24
	 assert false (* impossible to find element id in var list *)
25
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
26
    | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
27
    | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
28
    | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
29
    | Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
30
    | Expr_arrow (e1, e2) ->(
31
      match e1.expr_desc, e2.expr_desc with
32
      | Expr_const c1, Expr_const 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 *)
33
      | _ -> assert false (* only handle true -> false *)
34
    )
35
    | Expr_fby (e1, e2) -> assert false (* not covered yet *)
36
    | Expr_pre e -> fprintf fmt "UNITDELAY" 
37
    | Expr_when (e, id, l) -> assert false (* clocked based expressions are not handled yet *)
38
    | Expr_merge (id, hl) -> assert false (* clocked based expressions are not handled yet *)
39
    | Expr_appl (id, e, r) -> pp_app fmt id e r
40

  
41
  and pp_tuple fmt el =
42
    fprintf_list ~sep:"," pp_expr fmt el
43

  
44
  and pp_app fmt id e r =
45
    match r with
46
    | None -> pp_call fmt id e
47
    | Some c -> assert false (* clocked based expressions are not handled yet *)
48

  
49
  and pp_call fmt id e =
50
    match id, e.expr_desc with
51
    | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
52
    | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
53
    | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
54
    | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
55
    | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
56
    | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "mod (%a, %a)" pp_expr e1 pp_expr e2
57
    | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a & %a)" pp_expr e1 pp_expr e2
58
    | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a | %a)" pp_expr e1 pp_expr e2
59
    | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "xor (%a, %a)" pp_expr e1 pp_expr e2
60
    | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "((~%a) | %a)" pp_expr e1 pp_expr e2
61
    | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
62
    | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
63
    | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
64
    | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
65
    | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
66
    | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
67
    | "not", _ -> fprintf fmt "(~%a)" pp_expr e
68
    | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
69
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
70

  
71
  in
72
  pp_expr fmt expr
73

  
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
let pp_stmt fmt stmt =
95
  match stmt with
96
  | Eq eq -> (
97
    match eq.eq_lhs with
98
      [var] -> (
99
     (* first, we extract the expression and associated variables *)
100
	let vars = Utils.ISet.elements (Corelang.get_expr_vars eq.eq_rhs) in
101
	
102
	fprintf fmt "\"%s\": @[<v 2>{ \"expr\": \"%a\";@ \"vars\": [%a] @]}"
103
	  var
104
	  (pp_expr vars) eq.eq_rhs (* todo_pp_expr expr *)
105
	  (fprintf_list ~sep:", " pp_var_string) vars
106
      )
107
    | _ -> assert false (* should not happen for input of EMF backend (cocospec generated nodes *)
108
  )
109
  | _ -> assert false (* should not happen with EMF backend *)
110

  
111
let pp_node fmt nd =
112
  fprintf fmt "@[<v 2>\"%s\": {@ \"inputs\": [%a];@ \"outputs\": [%a];@ "
113
    nd.node_id
114
    pp_node_args nd.node_inputs
115
    pp_node_args nd.node_outputs;
116
  fprintf fmt "\"exprs\": {@[<v 1> %a@]@ }"
117
    (fprintf_list ~sep:";@ " pp_stmt ) nd.node_stmts;
118
  fprintf fmt "@]@ }"
119
    
120
let pp_decl fmt decl =
121
  match decl.top_decl_desc with
122
  | Node nd -> fprintf fmt "%a@ " pp_node nd
123
  | ImportedNode _ 
124
  | Const _
125
  | Open _ 
126
  | TypeDef _ -> eprintf "should not happen in EMF backend"
127

  
128

  
129
let translate fmt prog =
130
  fprintf fmt "@[<v 0>{@ ";
131
  fprintf_list ~sep:"@ " pp_decl fmt prog;
132
  fprintf fmt "@ @]}"
133

  
src/backends/EMF/EMF_backend.ml~
1
let translate fmt prog
src/corelang.ml
959 959
and get_node_calls nodes node =
960 960
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
961 961

  
962
let rec get_expr_vars vars e =
963
  get_expr_desc_vars vars e.expr_desc
964
and get_expr_desc_vars vars expr_desc =
962
let get_expr_vars e =
963
  let rec get_expr_vars vars e =
964
    get_expr_desc_vars vars e.expr_desc
965
  and get_expr_desc_vars vars expr_desc =
966
    Format.eprintf "get_expr_desc_vars expr=%a@." Printers.pp_expr (mkexpr Location.dummy_loc expr_desc);
965 967
  match expr_desc with
966 968
  | Expr_const _ -> vars
967
  | Expr_ident x -> Utils.ISet.add x vars
969
  | Expr_ident x -> Format.eprintf "%s is an ident!@." x; Utils.ISet.add x vars
968 970
  | Expr_tuple el
969 971
  | Expr_array el -> List.fold_left get_expr_vars vars el
970 972
  | Expr_pre e1 -> get_expr_vars vars e1
......
977 979
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
978 980
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
979 981
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
980

  
982
  in
983
  get_expr_vars Utils.ISet.empty e 
981 984

  
982 985
let rec expr_has_arrows e =
983 986
  expr_desc_has_arrows e.expr_desc
src/corelang.mli
118 118
val rename_static: (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_desc
119 119
val rename_carrier: (ident -> ident) -> clock_dec_desc -> clock_dec_desc
120 120

  
121
val get_expr_vars: Utils.ISet.t -> expr -> Utils.ISet.t
121
val get_expr_vars: expr -> Utils.ISet.t
122 122
val expr_replace_var: (ident -> ident) -> expr -> expr
123 123
val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
124 124

  
src/main_lustre_compiler.ml
90 90

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

  
96 96
(* From prog to prog *)
......
369 369
       (*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
370 370
       ()
371 371
     end
372
  | "emf" ->
373
     begin
374
       let destname = !Options.dest_dir ^ "/" ^ basename in
375
       let source_file = destname ^ ".emf" in (* Could be changed *)
376
       let source_out = open_out source_file in
377
       let fmt = formatter_of_out_channel source_out in
378
       EMF_backend.translate fmt prog;
379
       ()
380
     end
372 381

  
373 382
  | _ -> assert false
374 383

  
src/options.ml
75 75
    "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
76 76
    "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
77 77
    "-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";
78
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
78
    (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
79 79
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
80 80
    "-horn-traces", Arg.Unit (fun () -> output := "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
81 81
    "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
......
83 83
    "-horn-sfunction", Arg.Set_string sfunction, "Get the endpoint predicate of the sfunction";
84 84
    "-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
85 85
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
86
    "-emf", Arg.Unit (fun () -> output := "emf"), "generates EMF output, to be used by CocoSim";
86 87
    "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
87 88
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
88 89
    "-print_types", Arg.Set print_types, "prints node types";

Also available in: Unified diff