Project

General

Profile

Revision f0195e96

View differences:

configure.ac
78 78

  
79 79
# Seal
80 80
AC_MSG_CHECKING(seal library (optional))
81
AS_IF([ocamlfind query seal >/dev/null 2>&1; echo 1],
81
AS_IF([ocamlfind query seal >/dev/null 2>&1],
82 82
    [seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
83 83
)
84 84
AS_IF([test "x$seal" = "xyes"], [
85 85
   AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
86
   AC_SUBST(LUSTREV_SEAL_TAG, "") # <**/*>: package(seal)")
86
   AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
87
])
88

  
89
# Tiny
90
AC_MSG_CHECKING(tiny library (optional))
91
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
92
    [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
93
)
94
AS_IF([test "x$tiny" = "xyes"], [
95
 dnl   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)")
87 96
])
88 97

  
89 98
# z3 (optional)
......
125 134
])
126 135

  
127 136

  
128
# Tiny
129
AC_MSG_CHECKING(tiny library (optional))
130
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
131
    [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
132
)
137
dnl # Tiny
138
dnl AC_MSG_CHECKING(tiny library (optional))
139
dnl AS_IF([ocamlfind query tiny >/dev/null 2>&1],
140
dnl     [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
141
dnl )
133 142
AS_IF([test "x$tiny" = "xyes"], [
134 143
   AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
135
   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
144
   AC_SUBST(LUSTREV_TINY_TAG, ["<**/*>: package(apron.boxMPQ), package(apron.octMPQ), package(apron.polkaMPQ), package(tiny)"])
136 145
])
137 146

  
138 147
# Salsa
src/_tags.in
25 25
"tools/stateflow/json-parser": include
26 26
"tools/importer": include
27 27
"tools/seal": include
28
"tools/tiny": include
28 29

  
29 30
# svn
30 31
<**/.svn>: -traverse
......
36 37
<**/*verifier.native> or <**/*.ml{,i}> : package(yojson)
37 38

  
38 39
<**/*.native>                   : use_str
39
<**/main_lustre_compiler.native>: use_unix
40
<**/main_lustre_testgen.native> : use_unix
41
<**/main_lustre_verifier.native> : use_unix
42
<**/sf_sem.native>              : use_unix
40
<**/main_lustre_compiler.native>: package(unix)
41
<**/main_lustre_testgen.native> : package(unix)
42
<**/main_lustre_verifier.native> : package(unix)
43
<**/sf_sem.native>              : package(unix)
43 44
<**/*>                          : package(num)
45
<**/*>                          : package(zarith)
44 46
<**/*.ml>                       : package(logs)
45 47
<**/*.native>                   : package(logs)
46 48
<**/json_parser.ml>             : package(yojson)
src/backends/C/c_backend_common.ml
14 14
open Corelang
15 15
open Machine_code_types
16 16
(*open Machine_code_common*)
17

  
17
module Mpfr = Lustrec_mpfr
18 18

  
19 19
let print_version fmt =
20 20
  Format.fprintf fmt 
src/compiler_stages.ml
2 2
open Utils
3 3
open Compiler_common
4 4
open Lustre_types
5
module Mpfr = Lustrec_mpfr
5 6

  
6 7
exception StopPhase1 of program_t
7 8

  
src/machine_code_common.mli
22 22

  
23 23
val get_node_def: string -> Machine_code_types.machine_t -> Lustre_types.node_desc
24 24
val join_guards_list: Machine_code_types.instr_t list -> Machine_code_types.instr_t list
25
val machine_vars: Machine_code_types.machine_t -> Lustre_types.var_decl list
src/main_lustre_compiler.ml
52 52
    if !Options.mpfr &&
53 53
         extension = ".lus" (* trying to avoid the injection of the module for lusi files *) 
54 54
    then
55
      Mpfr.mpfr_module::prog
55
      Lustrec_mpfr.mpfr_module::prog
56 56
    else
57 57
      prog
58 58
  in
src/optimize_machine.ml
16 16
open Causality
17 17
open Machine_code_common
18 18
open Dimension
19
module Mpfr = Lustrec_mpfr
19 20

  
20 21

  
21 22
let pp_elim m fmt elim =
src/plugins/mpfr/lustrec_mpfr.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Utils
13
open Lustre_types
14
open Machine_code_types
15
open Corelang
16
open Normalization
17
open Machine_code_common
18

  
19
let report = Log.report ~plugin:"MPFR"
20
           
21
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
22
let cpt_fresh = ref 0
23
  
24
let mpfr_rnd () = "MPFR_RNDN"
25

  
26
let mpfr_prec () = !Options.mpfr_prec
27

  
28
let inject_id = "MPFRId"
29

  
30
let inject_copy_id = "mpfr_set"
31

  
32
let inject_real_id = "mpfr_set_flt"
33

  
34
let inject_init_id = "mpfr_init2"
35

  
36
let inject_clear_id = "mpfr_clear"
37

  
38
let mpfr_t = "mpfr_t"
39

  
40
let unfoldable_value value =
41
  not (Types.is_real_type value.value_type && is_const_value value)
42

  
43
let inject_id_id expr =
44
  let e = mkpredef_call expr.expr_loc inject_id [expr] in
45
  { e with
46
    expr_type = Type_predef.type_real;
47
    expr_clock = expr.expr_clock;
48
  }
49

  
50
let pp_inject_real pp_var pp_val fmt var value =
51
  Format.fprintf fmt "%s(%a, %a, %s);"
52
    inject_real_id
53
    pp_var var
54
    pp_val value
55
    (mpfr_rnd ())
56

  
57
let inject_assign expr =
58
  let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
59
  { e with
60
    expr_type = Type_predef.type_real;
61
    expr_clock = expr.expr_clock;
62
  }
63

  
64
let pp_inject_copy pp_var fmt var value =
65
  Format.fprintf fmt "%s(%a, %a, %s);"
66
    inject_copy_id
67
    pp_var var
68
    pp_var value
69
    (mpfr_rnd ())
70

  
71
let rec pp_inject_assign pp_var fmt var value =
72
  if is_const_value value
73
  then
74
    pp_inject_real pp_var pp_var fmt var value
75
  else
76
    pp_inject_copy pp_var fmt var value
77

  
78
let pp_inject_init pp_var fmt var =
79
  Format.fprintf fmt "%s(%a, %i);"
80
    inject_init_id
81
    pp_var var
82
    (mpfr_prec ())
83

  
84
let pp_inject_clear pp_var fmt var =
85
  Format.fprintf fmt "%s(%a);"
86
    inject_clear_id
87
    pp_var var
88

  
89
let base_inject_op id =
90
  match id with
91
  | "+"      -> "MPFRPlus"
92
  | "-"      -> "MPFRMinus"
93
  | "*"      -> "MPFRTimes"
94
  | "/"      -> "MPFRDiv"
95
  | "uminus" -> "MPFRUminus"
96
  | "<="     -> "MPFRLe"
97
  | "<"      -> "MPFRLt"
98
  | ">="     -> "MPFRGe"
99
  | ">"      -> "MPFRGt"
100
  | "="      -> "MPFREq"
101
  | "!="     -> "MPFRNeq"
102
  (* Conv functions *)
103
  | "int_to_real" -> "MPFRint_to_real"
104
  | "real_to_int" -> "MPFRreal_to_int"
105
  | "_floor" -> "MPFRfloor"        
106
  | "_ceil" -> "MPFRceil"        
107
  | "_round" -> "MPFRround"        
108
  | "_Floor" -> "MPFRFloor"        
109
  | "_Ceiling" -> "MPFRCeiling"        
110
  | "_Round" -> "MPFRRound"        
111
       
112
  (* Math library functions *)
113
  | "acos" -> "MPFRacos"
114
  | "acosh" -> "MPFRacosh"
115
  | "asin" -> "MPFRasin"
116
  | "asinh" -> "MPFRasinh"
117
  | "atan" -> "MPFRatan"
118
  | "atan2" -> "MPFRatan2"
119
  | "atanh" -> "MPFRatanh"
120
  | "cbrt" -> "MPFRcbrt"
121
  | "cos" -> "MPFRcos"
122
  | "cosh" -> "MPFRcosh"
123
  | "ceil" -> "MPFRceil"
124
  | "erf" -> "MPFRerf"
125
  | "exp" -> "MPFRexp"
126
  | "fabs" -> "MPFRfabs"
127
  | "floor" -> "MPFRfloor"
128
  | "fmod" -> "MPFRfmod"
129
  | "log" -> "MPFRlog"
130
  | "log10" -> "MPFRlog10"
131
  | "pow" -> "MPFRpow"
132
  | "round" -> "MPFRround"
133
  | "sin" -> "MPFRsin"
134
  | "sinh" -> "MPFRsinh"
135
  | "sqrt" -> "MPFRsqrt"
136
  | "trunc" -> "MPFRtrunc"
137
  | "tan" -> "MPFRtan"
138
  | _        -> raise Not_found
139

  
140
let inject_op id =
141
  report ~level:3 (fun fmt -> Format.fprintf fmt "trying to inject mpfr into function %s@." id);
142
  try
143
    base_inject_op id
144
  with Not_found -> id
145

  
146
let homomorphic_funs =
147
  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
148

  
149
let is_homomorphic_fun id =
150
  List.mem id homomorphic_funs
151

  
152
let inject_call expr =
153
  match expr.expr_desc with
154
  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
155
    { expr with expr_desc = Expr_appl (inject_op id, args, None) }
156
  | _ -> expr
157

  
158
let expr_of_const_array expr =
159
  match expr.expr_desc with
160
  | Expr_const (Const_array cl) ->
161
    let typ = Types.array_element_type expr.expr_type in
162
    let expr_of_const c =
163
      { expr_desc = Expr_const c;
164
	expr_type = typ;
165
	expr_clock = expr.expr_clock;
166
	expr_loc = expr.expr_loc;
167
	expr_delay = Delay.new_var ();
168
	expr_annot = None;
169
	expr_tag = new_tag ();
170
      }
171
    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
172
  | _                           -> assert false
173

  
174
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
175
let rec inject_list alias node inject_element defvars elist =
176
  List.fold_right
177
    (fun t (defvars, qlist) ->
178
      let defvars, norm_t = inject_element alias node defvars t in
179
      (defvars, norm_t :: qlist)
180
    ) elist (defvars, [])
181

  
182
let rec inject_expr ?(alias=true) node defvars expr =
183
let res =
184
  match expr.expr_desc with
185
  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr
186
  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
187
  | Expr_const (Const_struct _) -> assert false
188
  | Expr_ident _
189
  | Expr_const _  -> defvars, expr
190
  | Expr_array elist ->
191
    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
192
    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
193
    defvars, norm_expr
194
  | Expr_power (e1, d) ->
195
    let defvars, norm_e1 = inject_expr node defvars e1 in
196
    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
197
    defvars, norm_expr
198
  | Expr_access (e1, d) ->
199
    let defvars, norm_e1 = inject_expr node defvars e1 in
200
    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
201
    defvars, norm_expr
202
  | Expr_tuple elist -> 
203
    let defvars, norm_elist =
204
      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
205
    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
206
    defvars, norm_expr
207
  | Expr_appl (id, args, r) ->
208
    let defvars, norm_args = inject_expr node defvars args in
209
    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
210
    mk_expr_alias_opt alias node defvars (inject_call norm_expr)
211
  | Expr_arrow _ -> defvars, expr
212
  | Expr_pre e ->
213
    let defvars, norm_e = inject_expr node defvars e in
214
    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
215
    defvars, norm_expr
216
  | Expr_fby (e1, e2) ->
217
    let defvars, norm_e1 = inject_expr node defvars e1 in
218
    let defvars, norm_e2 = inject_expr node defvars e2 in
219
    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
220
    defvars, norm_expr
221
  | Expr_when (e, c, l) ->
222
    let defvars, norm_e = inject_expr node defvars e in
223
    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
224
    defvars, norm_expr
225
  | Expr_ite (c, t, e) ->
226
    let defvars, norm_c = inject_expr node defvars c in
227
    let defvars, norm_t = inject_expr node defvars t in
228
    let defvars, norm_e = inject_expr node defvars e in
229
    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
230
    defvars, norm_expr
231
  | Expr_merge (c, hl) ->
232
    let defvars, norm_hl = inject_branches node defvars hl in
233
    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
234
    defvars, norm_expr
235
in
236
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
237
res
238

  
239
and inject_branches node defvars hl =
240
 List.fold_right
241
   (fun (t, h) (defvars, norm_q) ->
242
     let (defvars, norm_h) = inject_expr node defvars h in
243
     defvars, (t, norm_h) :: norm_q
244
   )
245
   hl (defvars, [])
246

  
247

  
248
let rec inject_eq node defvars eq =
249
  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
250
  let norm_eq = { eq with eq_rhs = norm_rhs } in
251
  norm_eq::defs', vars'
252

  
253
(* let inject_eexpr ee =
254
 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
255
 *   
256
 * let inject_spec s =
257
 *   { s with
258
 *     assume = List.map inject_eexpr s.assume;
259
 *     guarantees = List.map inject_eexpr s.guarantees;
260
 *     modes = List.map (fun m ->
261
 *                 { m with
262
 *                   require = List.map inject_eexpr m.require;
263
 *                   ensure = List.map inject_eexpr m.ensure
264
 *                 }
265
 *               ) s.modes
266
 *   } *)
267
  
268
(** normalize_node node returns a normalized node, 
269
    ie. 
270
    - updated locals
271
    - new equations
272
    - 
273
*)
274
let inject_node node = 
275
  cpt_fresh := 0;
276
  let inputs_outputs = node.node_inputs@node.node_outputs in
277
  let norm_ctx = (node.node_id, get_node_vars node) in
278
  let is_local v =
279
    List.for_all ((!=) v) inputs_outputs in
280
  let orig_vars = inputs_outputs@node.node_locals in
281
  let defs, vars =
282
    let eqs, auts = get_node_eqs node in
283
    if auts != [] then assert false; (* Automata should be expanded by now. *)
284
    List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in
285
  (* Normalize the asserts *)
286
  let vars, assert_defs, asserts = 
287
    List.fold_left (
288
    fun (vars, def_accu, assert_accu) assert_ ->
289
      let assert_expr = assert_.assert_expr in
290
      let (defs, vars'), expr = 
291
	inject_expr 
292
	  ~alias:false 
293
	  norm_ctx 
294
	  ([], vars) (* defvar only contains vars *)
295
	  assert_expr
296
      in
297
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
298
    ) (vars, [], []) node.node_asserts in
299
  let new_locals = List.filter is_local vars in
300
  (* Compute traceability info: 
301
     - gather newly bound variables
302
     - compute the associated expression without aliases     
303
  *)
304
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
305
  (* See comment below
306
   *  let spec = match node.node_spec with
307
   *   | None -> None
308
   *   | Some spec -> Some (inject_spec spec)
309
   * in *)
310
  let node =
311
  { node with 
312
    node_locals = new_locals; 
313
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
314
    (* Incomplete work: TODO. Do we have to inject MPFR code here?
315
       Does it make sense for annotations? For me, only if we produce
316
       C code for annotations. Otherwise the various verification
317
       backend should have their own understanding, but would not
318
       necessarily require this additional normalization. *)
319
    (* 
320
       node_spec = spec;
321
       node_annot = List.map (fun ann -> {ann with
322
           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
323
         ) node.node_annot *)
324
  }
325
  in ((*Printers.pp_node Format.err_formatter node;*) node)
326

  
327
let inject_decl decl =
328
  match decl.top_decl_desc with
329
  | Node nd ->
330
    {decl with top_decl_desc = Node (inject_node nd)}
331
  | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
332
  
333
let inject_prog decls = 
334
  List.map inject_decl decls
335

  
336

  
337
(* Local Variables: *)
338
(* compile-command:"make -C .." *)
339
(* End: *)
src/plugins/mpfr/mpfr.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
open Utils
13
open Lustre_types
14
open Machine_code_types
15
open Corelang
16
open Normalization
17
open Machine_code_common
18

  
19
let report = Log.report ~plugin:"MPFR"
20
           
21
let mpfr_module = mktop (Open(false, "mpfr_lustre"))
22
let cpt_fresh = ref 0
23
  
24
let mpfr_rnd () = "MPFR_RNDN"
25

  
26
let mpfr_prec () = !Options.mpfr_prec
27

  
28
let inject_id = "MPFRId"
29

  
30
let inject_copy_id = "mpfr_set"
31

  
32
let inject_real_id = "mpfr_set_flt"
33

  
34
let inject_init_id = "mpfr_init2"
35

  
36
let inject_clear_id = "mpfr_clear"
37

  
38
let mpfr_t = "mpfr_t"
39

  
40
let unfoldable_value value =
41
  not (Types.is_real_type value.value_type && is_const_value value)
42

  
43
let inject_id_id expr =
44
  let e = mkpredef_call expr.expr_loc inject_id [expr] in
45
  { e with
46
    expr_type = Type_predef.type_real;
47
    expr_clock = expr.expr_clock;
48
  }
49

  
50
let pp_inject_real pp_var pp_val fmt var value =
51
  Format.fprintf fmt "%s(%a, %a, %s);"
52
    inject_real_id
53
    pp_var var
54
    pp_val value
55
    (mpfr_rnd ())
56

  
57
let inject_assign expr =
58
  let e = mkpredef_call expr.expr_loc inject_copy_id [expr] in
59
  { e with
60
    expr_type = Type_predef.type_real;
61
    expr_clock = expr.expr_clock;
62
  }
63

  
64
let pp_inject_copy pp_var fmt var value =
65
  Format.fprintf fmt "%s(%a, %a, %s);"
66
    inject_copy_id
67
    pp_var var
68
    pp_var value
69
    (mpfr_rnd ())
70

  
71
let rec pp_inject_assign pp_var fmt var value =
72
  if is_const_value value
73
  then
74
    pp_inject_real pp_var pp_var fmt var value
75
  else
76
    pp_inject_copy pp_var fmt var value
77

  
78
let pp_inject_init pp_var fmt var =
79
  Format.fprintf fmt "%s(%a, %i);"
80
    inject_init_id
81
    pp_var var
82
    (mpfr_prec ())
83

  
84
let pp_inject_clear pp_var fmt var =
85
  Format.fprintf fmt "%s(%a);"
86
    inject_clear_id
87
    pp_var var
88

  
89
let base_inject_op id =
90
  match id with
91
  | "+"      -> "MPFRPlus"
92
  | "-"      -> "MPFRMinus"
93
  | "*"      -> "MPFRTimes"
94
  | "/"      -> "MPFRDiv"
95
  | "uminus" -> "MPFRUminus"
96
  | "<="     -> "MPFRLe"
97
  | "<"      -> "MPFRLt"
98
  | ">="     -> "MPFRGe"
99
  | ">"      -> "MPFRGt"
100
  | "="      -> "MPFREq"
101
  | "!="     -> "MPFRNeq"
102
  (* Conv functions *)
103
  | "int_to_real" -> "MPFRint_to_real"
104
  | "real_to_int" -> "MPFRreal_to_int"
105
  | "_floor" -> "MPFRfloor"        
106
  | "_ceil" -> "MPFRceil"        
107
  | "_round" -> "MPFRround"        
108
  | "_Floor" -> "MPFRFloor"        
109
  | "_Ceiling" -> "MPFRCeiling"        
110
  | "_Round" -> "MPFRRound"        
111
       
112
  (* Math library functions *)
113
  | "acos" -> "MPFRacos"
114
  | "acosh" -> "MPFRacosh"
115
  | "asin" -> "MPFRasin"
116
  | "asinh" -> "MPFRasinh"
117
  | "atan" -> "MPFRatan"
118
  | "atan2" -> "MPFRatan2"
119
  | "atanh" -> "MPFRatanh"
120
  | "cbrt" -> "MPFRcbrt"
121
  | "cos" -> "MPFRcos"
122
  | "cosh" -> "MPFRcosh"
123
  | "ceil" -> "MPFRceil"
124
  | "erf" -> "MPFRerf"
125
  | "exp" -> "MPFRexp"
126
  | "fabs" -> "MPFRfabs"
127
  | "floor" -> "MPFRfloor"
128
  | "fmod" -> "MPFRfmod"
129
  | "log" -> "MPFRlog"
130
  | "log10" -> "MPFRlog10"
131
  | "pow" -> "MPFRpow"
132
  | "round" -> "MPFRround"
133
  | "sin" -> "MPFRsin"
134
  | "sinh" -> "MPFRsinh"
135
  | "sqrt" -> "MPFRsqrt"
136
  | "trunc" -> "MPFRtrunc"
137
  | "tan" -> "MPFRtan"
138
  | _        -> raise Not_found
139

  
140
let inject_op id =
141
  report ~level:3 (fun fmt -> Format.fprintf fmt "trying to inject mpfr into function %s@." id);
142
  try
143
    base_inject_op id
144
  with Not_found -> id
145

  
146
let homomorphic_funs =
147
  List.fold_right (fun id res -> try base_inject_op id :: res with Not_found -> res) Basic_library.internal_funs []
148

  
149
let is_homomorphic_fun id =
150
  List.mem id homomorphic_funs
151

  
152
let inject_call expr =
153
  match expr.expr_desc with
154
  | Expr_appl (id, args, None) when not (Basic_library.is_expr_internal_fun expr) ->
155
    { expr with expr_desc = Expr_appl (inject_op id, args, None) }
156
  | _ -> expr
157

  
158
let expr_of_const_array expr =
159
  match expr.expr_desc with
160
  | Expr_const (Const_array cl) ->
161
    let typ = Types.array_element_type expr.expr_type in
162
    let expr_of_const c =
163
      { expr_desc = Expr_const c;
164
	expr_type = typ;
165
	expr_clock = expr.expr_clock;
166
	expr_loc = expr.expr_loc;
167
	expr_delay = Delay.new_var ();
168
	expr_annot = None;
169
	expr_tag = new_tag ();
170
      }
171
    in { expr with expr_desc = Expr_array (List.map expr_of_const cl) }
172
  | _                           -> assert false
173

  
174
(* inject_<foo> : defs * used vars -> <foo> -> (updated defs * updated vars) * normalized <foo> *)
175
let rec inject_list alias node inject_element defvars elist =
176
  List.fold_right
177
    (fun t (defvars, qlist) ->
178
      let defvars, norm_t = inject_element alias node defvars t in
179
      (defvars, norm_t :: qlist)
180
    ) elist (defvars, [])
181

  
182
let rec inject_expr ?(alias=true) node defvars expr =
183
let res =
184
  match expr.expr_desc with
185
  | Expr_const (Const_real _)  -> mk_expr_alias_opt alias node defvars expr
186
  | Expr_const (Const_array _) -> inject_expr ~alias:alias node defvars (expr_of_const_array expr)
187
  | Expr_const (Const_struct _) -> assert false
188
  | Expr_ident _
189
  | Expr_const _  -> defvars, expr
190
  | Expr_array elist ->
191
    let defvars, norm_elist = inject_list alias node (fun _ -> inject_expr ~alias:true) defvars elist in
192
    let norm_expr = { expr with expr_desc = Expr_array norm_elist } in
193
    defvars, norm_expr
194
  | Expr_power (e1, d) ->
195
    let defvars, norm_e1 = inject_expr node defvars e1 in
196
    let norm_expr = { expr with expr_desc = Expr_power (norm_e1, d) } in
197
    defvars, norm_expr
198
  | Expr_access (e1, d) ->
199
    let defvars, norm_e1 = inject_expr node defvars e1 in
200
    let norm_expr = { expr with expr_desc = Expr_access (norm_e1, d) } in
201
    defvars, norm_expr
202
  | Expr_tuple elist -> 
203
    let defvars, norm_elist =
204
      inject_list alias node (fun alias -> inject_expr ~alias:alias) defvars elist in
205
    let norm_expr = { expr with expr_desc = Expr_tuple norm_elist } in
206
    defvars, norm_expr
207
  | Expr_appl (id, args, r) ->
208
    let defvars, norm_args = inject_expr node defvars args in
209
    let norm_expr = { expr with expr_desc = Expr_appl (id, norm_args, r) } in
210
    mk_expr_alias_opt alias node defvars (inject_call norm_expr)
211
  | Expr_arrow _ -> defvars, expr
212
  | Expr_pre e ->
213
    let defvars, norm_e = inject_expr node defvars e in
214
    let norm_expr = { expr with expr_desc = Expr_pre norm_e } in
215
    defvars, norm_expr
216
  | Expr_fby (e1, e2) ->
217
    let defvars, norm_e1 = inject_expr node defvars e1 in
218
    let defvars, norm_e2 = inject_expr node defvars e2 in
219
    let norm_expr = { expr with expr_desc = Expr_fby (norm_e1, norm_e2) } in
220
    defvars, norm_expr
221
  | Expr_when (e, c, l) ->
222
    let defvars, norm_e = inject_expr node defvars e in
223
    let norm_expr = { expr with expr_desc = Expr_when (norm_e, c, l) } in
224
    defvars, norm_expr
225
  | Expr_ite (c, t, e) ->
226
    let defvars, norm_c = inject_expr node defvars c in
227
    let defvars, norm_t = inject_expr node defvars t in
228
    let defvars, norm_e = inject_expr node defvars e in
229
    let norm_expr = { expr with expr_desc = Expr_ite (norm_c, norm_t, norm_e) } in
230
    defvars, norm_expr
231
  | Expr_merge (c, hl) ->
232
    let defvars, norm_hl = inject_branches node defvars hl in
233
    let norm_expr = { expr with expr_desc = Expr_merge (c, norm_hl) } in
234
    defvars, norm_expr
235
in
236
(*Format.eprintf "inject_expr %B %a = %a@." alias Printers.pp_expr expr Printers.pp_expr (snd res);*)
237
res
238

  
239
and inject_branches node defvars hl =
240
 List.fold_right
241
   (fun (t, h) (defvars, norm_q) ->
242
     let (defvars, norm_h) = inject_expr node defvars h in
243
     defvars, (t, norm_h) :: norm_q
244
   )
245
   hl (defvars, [])
246

  
247

  
248
let rec inject_eq node defvars eq =
249
  let (defs', vars'), norm_rhs = inject_expr ~alias:false node defvars eq.eq_rhs in
250
  let norm_eq = { eq with eq_rhs = norm_rhs } in
251
  norm_eq::defs', vars'
252

  
253
(* let inject_eexpr ee =
254
 *   { ee with eexpr_qfexpr = inject_expr ee.eexpr_qfexpr }
255
 *   
256
 * let inject_spec s =
257
 *   { s with
258
 *     assume = List.map inject_eexpr s.assume;
259
 *     guarantees = List.map inject_eexpr s.guarantees;
260
 *     modes = List.map (fun m ->
261
 *                 { m with
262
 *                   require = List.map inject_eexpr m.require;
263
 *                   ensure = List.map inject_eexpr m.ensure
264
 *                 }
265
 *               ) s.modes
266
 *   } *)
267
  
268
(** normalize_node node returns a normalized node, 
269
    ie. 
270
    - updated locals
271
    - new equations
272
    - 
273
*)
274
let inject_node node = 
275
  cpt_fresh := 0;
276
  let inputs_outputs = node.node_inputs@node.node_outputs in
277
  let norm_ctx = (node.node_id, get_node_vars node) in
278
  let is_local v =
279
    List.for_all ((!=) v) inputs_outputs in
280
  let orig_vars = inputs_outputs@node.node_locals in
281
  let defs, vars =
282
    let eqs, auts = get_node_eqs node in
283
    if auts != [] then assert false; (* Automata should be expanded by now. *)
284
    List.fold_left (inject_eq norm_ctx) ([], orig_vars) eqs in
285
  (* Normalize the asserts *)
286
  let vars, assert_defs, asserts = 
287
    List.fold_left (
288
    fun (vars, def_accu, assert_accu) assert_ ->
289
      let assert_expr = assert_.assert_expr in
290
      let (defs, vars'), expr = 
291
	inject_expr 
292
	  ~alias:false 
293
	  norm_ctx 
294
	  ([], vars) (* defvar only contains vars *)
295
	  assert_expr
296
      in
297
      vars', defs@def_accu, {assert_ with assert_expr = expr}::assert_accu
298
    ) (vars, [], []) node.node_asserts in
299
  let new_locals = List.filter is_local vars in
300
  (* Compute traceability info: 
301
     - gather newly bound variables
302
     - compute the associated expression without aliases     
303
  *)
304
  (* let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals)) new_locals in *)
305
  (* See comment below
306
   *  let spec = match node.node_spec with
307
   *   | None -> None
308
   *   | Some spec -> Some (inject_spec spec)
309
   * in *)
310
  let node =
311
  { node with 
312
    node_locals = new_locals; 
313
    node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
314
    (* Incomplete work: TODO. Do we have to inject MPFR code here?
315
       Does it make sense for annotations? For me, only if we produce
316
       C code for annotations. Otherwise the various verification
317
       backend should have their own understanding, but would not
318
       necessarily require this additional normalization. *)
319
    (* 
320
       node_spec = spec;
321
       node_annot = List.map (fun ann -> {ann with
322
           annots = List.map (fun (ids, ee) -> ids, inject_eexpr ee) ann.annots}
323
         ) node.node_annot *)
324
  }
325
  in ((*Printers.pp_node Format.err_formatter node;*) node)
326

  
327
let inject_decl decl =
328
  match decl.top_decl_desc with
329
  | Node nd ->
330
    {decl with top_decl_desc = Node (inject_node nd)}
331
  | Include _ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
332
  
333
let inject_prog decls = 
334
  List.map inject_decl decls
335

  
336

  
337
(* Local Variables: *)
338
(* compile-command:"make -C .." *)
339
(* End: *)
src/real.ml
16 16
  let num_10 = Num.num_of_int 10 in
17 17
  Num.(c // (num_10 **/ (num_of_int e)))
18 18

  
19
let rec to_q (c, e, s) =
20
  if e = 0 then
21
        Q.of_string (Num.string_of_num c)
22
  else
23
    if e > 0 then Q.div (to_q (c,e-1,s)) (Q.of_int 10)
24
    else (* if exp<0 then *)
25
      Q.mul
26
        (to_q (c,e+1,s))
27
        (Q.of_int 10)
28

  
19 29
let to_string (_, _, s) = s
20 30
                        
21 31
let eq r1 r2 =
src/real.mli
18 18
val diseq: t -> t -> bool
19 19
  
20 20
val to_num: t -> Num.num
21
val to_q: t -> Q.t
21 22
val to_string: t -> string
22 23
val eq: t -> t -> bool
23 24
val zero: t
src/tools/tiny/tiny_utils.ml
1

  
2
module Ast = Tiny.Ast
3

  
4

  
5
let lloc_to_tloc loc = Tiny.Location.dummy (*TODO*)
6
                     
7
let tloc_to_lloc loc = Location.dummy_loc (*TODO*)
8

  
9
                     
10
let ltyp_to_ttyp t =
11
  if Types.is_real_type t then Tiny.Ast.RealT
12
  else if Types.is_int_type t then Tiny.Ast.IntT
13
  else if Types.is_bool_type t then Tiny.Ast.BoolT
14
  else assert false (* not covered yet *)
15

  
16
let cst_bool loc b =
17
  { Ast.expr_desc =
18
      if b then
19
        Ast.Cst(Q.of_int 1, "true")
20
      else
21
        Ast.Cst(Q.of_int 0, "false");
22
    expr_loc = loc;
23
    expr_type = Ast.BoolT }
24
  
25
let rec real_to_q man exp =
26
  if exp = 0 then
27
        Q.of_string (Num.string_of_num man)
28
  else
29
    if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
30
    else (* if exp<0 then *)
31
      Q.mul
32
        (real_to_q man (exp+1))
33
        (Q.of_int 10)
34

  
35
let instr_loc i =
36
  match i.Machine_code_types.lustre_eq with
37
  | None -> Tiny.Location.dummy
38
  | Some eq -> lloc_to_tloc eq.eq_loc
39
             
40
let rec lval_to_texpr loc _val =
41
  let build d v =
42
      Ast.{ expr_desc = d;
43
            expr_loc = loc;
44
            expr_type = v }
45
  in
46
  let new_desc =
47
    match _val.Machine_code_types.value_desc with
48
  | Machine_code_types.Cst cst -> (
49
    match cst with
50
      Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
51
    | Const_real r -> Ast.Cst (Real.to_q r, Real.to_string r) 
52
      | _ -> assert false
53
  )
54
     
55
  | Var v -> Ast.Var (v.var_id)
56
  | Fun (op, vl) ->
57
     let t_arg = match vl with
58
       | hd::_ -> ltyp_to_ttyp hd.value_type
59
       | _ -> assert false
60
     in
61
     (
62
       match op, List.map (lval_to_texpr loc) vl with
63
       | "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2)
64
       | "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2)
65
       | "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2)
66
       | "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2)
67
       | "<", [v1;v2] ->
68
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
69
       | "<=", [v1;v2] ->
70
          Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
71
       | ">", [v1;v2] ->
72
          Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
73
       | ">=", [v1;v2] ->
74
          Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
75
       | "=", [v1;v2] ->
76
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
77
       | "!=", [v1;v2] ->
78
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
79
       | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
80
  )
81
  | _ -> assert false (* no array. access or power *)
82
  in
83
  build new_desc (ltyp_to_ttyp _val.value_type)
84

  
85
  
86
let machine_body_to_ast init m =
87
  let init_var = ref None in
88
  let rec guarded_expr_to_stm loc te guarded_instrs =
89
    match guarded_instrs with
90
    | [] -> assert false
91
    | [_,il] -> instrl_to_stm il
92
    | (label, il)::tl ->
93
       let stmt = instrl_to_stm il in
94
       let guard= match label with
95
           "true" -> te
96
         | "false" -> Ast.neg_guard te
97
         | _ -> assert false (* TODO: don't deal with non boolean
98
                                guards. Could just treturn true and
99
                                over-approximate behavior *)
100
       in
101
       if (match !init_var, te.Ast.expr_desc with
102
           | Some v, Var v2 -> v = v2
103
           | _ -> false) then 
104
         instrl_to_stm (
105
             if init then
106
               (List.assoc "true" guarded_instrs)
107
             else
108
               (List.assoc "false" guarded_instrs)
109
           )
110
       else
111
         Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl)
112
  and instr_to_stm i =
113
    let loc = instr_loc i in
114
    match i.instr_desc with
115
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
116
       Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
117
    | MBranch (e, guarded_instrs) -> (
118
      let te = lval_to_texpr loc e in
119
      guarded_expr_to_stm loc te guarded_instrs
120
    )
121
    | MStep (ol, id, args) ->
122
       if List.mem_assoc id m.Machine_code_types.minstances then
123
         let fun_name, _ = List.assoc id m.minstances in
124
         match Corelang.node_name fun_name, ol with
125
         | "_arrow", [o] -> (
126
           init_var := Some o.var_id;
127
           Ast.Nop (loc);
128
             (* Ast.Asn (loc, o.var_id, 
129
              *        { expr_desc =              if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false");
130
              *          expr_loc = loc;
131
              *          expr_type = Ast.BoolT }
132
              * ) *)
133
         )
134
         | name, _ -> 
135
            (
136
              Format.eprintf "No tiny translation for node call  %s@.@?" name;
137
              assert false
138
            )
139
       else (
140
         Format.eprintf "No tiny translation for node call  %s@.@?" id;
141
         assert false
142
       )
143
    | MReset id
144
      | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
145
    | MComment s 
146
      | MSpec s -> assert false
147
  and instrl_to_stm il =
148
    match il with
149
      [] -> assert false
150
    | [i] -> instr_to_stm i
151
    | i::il ->
152
       let i' = instr_to_stm i in
153
       Ast.Seq (instr_loc i, i', (instrl_to_stm il))
154
  in
155
  instrl_to_stm m.Machine_code_types.mstep.step_instrs 
156

  
157
let read_var loc bounds_opt v =
158
  let min, max =
159
    match bounds_opt with
160
      Some (min,max) -> min, max
161
    | None -> (Q.of_int (-1), "-1"), (Q.of_int 1, "1")
162
  in
163
  let range = {
164
      Ast.expr_desc = Ast.Rand (min,max);
165
      expr_loc = loc;
166
      expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
167
    }
168
  in
169
  Ast.Asn (loc, v.var_id, range)
170
  
171
let rec read_vars loc bounds_inputs vl =
172
  match vl with
173
    [] -> Ast.Nop loc
174
  | [v] -> read_var
175
             loc
176
             (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
177
                Some (List.assoc v.Lustre_types.var_id bounds_inputs)
178
              else
179
                None)
180
             v
181
  | v::tl ->
182
     Ast.Seq (loc,
183
              read_var
184
                loc
185
                (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
186
                   Some (List.assoc v.Lustre_types.var_id bounds_inputs)
187
                 else
188
                   None)
189
                v,
190
              read_vars loc bounds_inputs tl
191
       )
192
  
193
let machine_to_ast bounds_input m =
194
  let loc = Tiny.Location.dummy in
195
  let read_vars = read_vars loc bounds_input m.Machine_code_types.mstep.step_inputs in
196
  let ast_loop_first = machine_body_to_ast true m in
197
  let ast_loop_run = machine_body_to_ast false m in
198
  let ast_loop_body = Ast.Seq (loc, read_vars, ast_loop_run) in
199
  let loop = Ast.While(loc, cst_bool loc true, ast_loop_body) in
200
  Ast.Seq (loc, read_vars, (Ast.Seq (loc, ast_loop_first, loop)))
201
  
202
let machine_to_env m =
203
  
204
    List.fold_left (fun accu v ->
205
      let typ =
206
        ltyp_to_ttyp (v.Lustre_types.var_type)
207
      in
208
      Ast.VarSet.add (v.var_id, typ) accu)
209
    Ast.VarSet.empty
210
    (Machine_code_common.machine_vars m)
211

  
src/tools/tiny/tiny_verifier.ml
1

  
2
let active = ref false
3
let tiny_debug = ref false
4

  
5
    
6
let tiny_run ~basename prog machines =
7
  let node_name =
8
    match !Options.main_node with
9
    | "" -> (
10
      Format.eprintf "Tiny verifier requires a main node.@.";
11
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
12
        (Utils.fprintf_list ~sep:"@ "
13
           (fun fmt m ->
14
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
15
           )
16
        )
17
        machines; 
18
      exit 1
19
    )
20
    | s -> ( (* should have been addessed before *)
21
      match Machine_code_common.get_machine_opt machines s with
22
      | None -> begin
23
          Global.main_node := s;
24
          Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
25
          raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
26
        end
27
      | Some _ -> s
28
    )
29
  in
30
  let m = Machine_code_common.get_machine machines node_name in
31
  let env = (* We add each variables of the node the Tiny env *)
32
    Tiny_utils.machine_to_env m in
33
  let nd = m.mname in
34
  (* Building preamble with some bounds on inputs *)
35
  (* TODO: deal woth contracts, asserts, ... *)
36
  let bounds_inputs = [] in
37
  let ast = Tiny_utils.machine_to_ast bounds_inputs m in
38
  let mems = m.mmemory in
39
  
40
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
41

  
42
  ()
43
  
44
  
45
module Verifier =
46
  (struct
47
    include VerifierType.Default
48
    let name = "tiny"
49
    let options =
50
      [
51
        "-debug", Arg.Set tiny_debug, "tiny debug"
52
      ]
53
      
54
    let activate () =
55
      active := true;
56
      (* Options.global_inline := true;
57
       * Options.optimization := 0;
58
       * Options.const_unfold := true; *)
59
      ()
60
      
61
    let is_active () = !active
62
    let run = tiny_run
63
            
64
            
65
  end: VerifierType.S)
66
    

Also available in: Unified diff