Project

General

Profile

Revision ad4774b0

View differences:

Makefile.in
8 8
LUSI_MPFR_LIB=include/mpfr_lustre.lusi
9 9
LOCAL_BINDIR=bin
10 10
LOCAL_DOCDIR=doc/manual
11
BIN_TARGETS = lustrec lustret @lustresf_target@
11
BIN_TARGETS = lustrec lustret lustrev @lustresf_target@
12 12

  
13 13
DEFAULT_TEST_TARGET=COMPIL_LUS\|MAKE\|BIN\|DIFF
14 14
DEFAULT_EXCLUDE_TEST=LUSTRET
......
23 23
	@echo Compiling binary lustret
24 24
	@make -C src lustret
25 25

  
26
lustrev:
27
	@echo Compiling binary lustrev
28
	@make -C src lustrev
29

  
26 30
@lustresf@
27 31

  
28 32
configure: configure.ac
configure.ac
55 55

  
56 56
# Checks for libraries.
57 57
# OCamlgraph
58
AC_MSG_CHECKING(ocaml libraries required)
58
AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num)) 
59 59
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1],
60 60
    [],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)],
61 61
)
......
67 67
    [yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)],
68 68
)
69 69

  
70
# Seal
71
AC_MSG_CHECKING(seal library (optional))
72
AS_IF([ocamlfind query seal >/dev/null 2>&1],
73
    [seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
74
)
75
AS_IF([test "x$seal" = "xyes"], [
76
   AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
77
   AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
78
])
79

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

  
90
# Tiny
91
AC_MSG_CHECKING(tiny library (optional))
92
AS_IF([ocamlfind query tiny >/dev/null 2>&1],
93
    [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
94
)
95
AS_IF([test "x$tiny" = "xyes"], [
96
   AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
97
   AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
98
])
99

  
70 100
# Salsa
71 101
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
72 102
              [disable Salsa plugin. Enabled by default if available.])])
......
79 109

  
80 110
AS_IF([test "x$enable_salsa" != "xno"], [
81 111
  if (test "x$salsa" = xyes ); then
82
   AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.PluginType);")
112
   AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
83 113
   AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)")
84 114
  fi
85 115
])
......
156 186
		 src/Makefile
157 187
		 src/version.ml
158 188
		 src/pluginList.ml
189
		 src/verifierList.ml
159 190
		 src/_tags
160 191
		 src/ocaml_utils.ml
161 192
		 ])
......
190 221
        AC_MSG_NOTICE([lustresf not available])
191 222
      fi
192 223
  fi
224
AC_MSG_NOTICE(********   Verifiers    ********)
225

  
226
  if (test "x$seal" = "xyes"); then
227
      AC_MSG_NOTICE([Seal   enabled])
228
  else
229
      AC_MSG_NOTICE([Seal   disabled. Require Seal library])
230
  fi
231

  
232
  if (test "x$z3" = xyes); then
233
      AC_MSG_NOTICE([Zustre enabled])
234
  else
235
      AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
236
  fi
237

  
238
  if (test "x$tiny" = xyes); then
239
      AC_MSG_NOTICE([Tiny   enabled])
240
  else
241
      AC_MSG_NOTICE([Tiny   disabled. Require Tiny library])
242
  fi
193 243

  
194 244
AC_MSG_NOTICE(****** Regression Tests  ******)
195 245
if (test "x$valid_test_path" = xfalse); then
src/Makefile.in
10 10
LOCAL_BINDIR=../bin
11 11
LOCAL_DOCDIR=../doc/manual
12 12

  
13
all: lustrec lustret
13
all: lustrec lustret lustrev
14 14

  
15 15
lustrec:
16 16
	@echo Compiling binary lustrec
......
24 24
	@mkdir -p $(LOCAL_BINDIR)
25 25
	@mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
26 26

  
27
lustrev:
28
	@echo Compiling binary lustrev
29
	@$(OCAMLBUILD) main_lustre_verifier.native
30
	@mkdir -p $(LOCAL_BINDIR)
31
	@mv _build/main_lustre_verifier.native $(LOCAL_BINDIR)/lustrev
32

  
27 33
@lustresf_src@
28 34

  
29 35
doc:
......
47 53
install:
48 54
	make -C .. install
49 55

  
50
.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean tests
56
.PHONY: compile-lusi doc dot lustrec lustret lustrev lustrec.odocl clean install dist-clean tests
src/_tags.in
10 10
"plugins/scopes": include
11 11
"plugins/mpfr": include
12 12
"features/machine_types": include
13
"tools": include
13 14
"tools/stateflow": include
14 15
"tools/stateflow/common": include
15 16
"tools/stateflow/semantics": include
......
23 24
# packages
24 25
<**/*.native>                   : package(ocamlgraph)
25 26
<**/*.native>                   : use_str
26
<**/main_lustre_compiler.native>: use_unix
27
<**/main_lustre_testgen.native> : use_unix
28
<**/sf_sem.native>              : use_unix
27
<**/*.native>                   : use_unix
29 28
<**/*.native>                   : package(num)
30 29
<**/*.ml>                       : package(logs)
31 30
<**/*.native>                   : package(logs)
......
45 44
# Plugin dependencies
46 45
@SALSA_TAG@
47 46

  
47
# Available solvers
48
@LUSTREV_SEAL_TAG@
49
@LUSTREV_TINY_TAG@
50
@LUSTREV_Z3_TAG@
51

  
48 52
# Local Variables:
49 53
# mode: conf
50 54
# End:
src/algebraicLoop.ml
157 157
  (* Clock calculus *)
158 158
  let _ (*computed_clocks_env*) = Compiler_common.clock_decls clock_env prog in
159 159
  (* Normalization *)
160
  let prog = Normalization.normalize_prog ~backend:!Options.output prog in
160
  let params = Backends.get_normalization_params () in
161
  let prog = Normalization.normalize_prog params prog in
161 162
  (* Mini stage 2 : Scheduling *)
162 163
  let res = Scheduling.schedule_prog prog in
163 164
  Options.verbose_level := !Options.verbose_level + 2;
......
272 273
    Alarms contain the list of inlining performed or advised for each node. 
273 274
    This could be provided as a feedback to the user.
274 275
*)
275
let clean_al prog : program * bool * report =
276
let clean_al prog : program_t * bool * report =
276 277
  let max_inlines = !Options.al_nb_max in
277 278
(* We iterate over each node *)
278 279
  let _, prog, al_list =
src/backends/backends.ml
16 16
  | "horn" | "lustre" | "acsl" | "emf" -> true
17 17
  | _ -> false
18 18

  
19
                             
20
(* Special treatment of arrows in lustre backend. We want to keep them *)
21
let unfold_arrow () =
22
  match !Options.output with
23
  | "lustre" -> false
24
  | _ -> true
25

  
26
(* Forcing ite normalization *)
27
let alias_ite () =
28
  match !Options.output with
29
  | "emf" -> true
30
  | _ -> false
31

  
32
(* Forcing basic functions normalization *)
33
let alias_internal_fun () =
34
  match !Options.output with
35
  | "emf" -> true
36
  | _ -> false
37

  
38
let get_normalization_params () = {
39
    Normalization.unfold_arrow_active = unfold_arrow ();
40
    force_alias_ite = alias_ite ();
41
    force_alias_internal_fun = alias_internal_fun ();
42
  }
43

  
19 44

  
20 45
(* Local Variables: *)
21 46
(* compile-command: "make -k -C .." *)
src/compiler_stages.ml
3 3
open Compiler_common
4 4
open LustreSpec
5 5

  
6
exception StopPhase1 of program
6
exception StopPhase1 of program_t
7 7

  
8 8
let dynamic_checks () =
9 9
  match !Options.output, !Options.spec with
......
22 22
      begin
23 23
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
24 24
	Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
25
	Lusic.print_lusic_to_h destname lusic_ext
25
	if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
26 26
      end
27 27
    else
28 28
      let lusic = Lusic.read_lusic destname lusic_ext in
......
31 31
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
32 32
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
33 33
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
34
	  Lusic.print_lusic_to_h destname lusic_ext
34
	  if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
35 35
	end
36 36
      else
37 37
	begin
......
47 47

  
48 48

  
49 49
(* From prog to prog *)
50
let stage1 prog dirname basename =
50
let stage1 params prog dirname basename =
51 51
  (* Updating parent node information for variables *)
52 52
  Compiler_common.update_vdecl_parents_prog prog;
53 53

  
......
175 175

  
176 176
  (* Normalization phase *)
177 177
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
178
  let prog = Normalization.normalize_prog ~backend:!Options.output prog in
178
  let prog = Normalization.normalize_prog params prog in
179 179
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
180 180

  
181 181
  let prog =
src/corelang.mli
110 110

  
111 111
val add_internal_funs: unit -> unit
112 112

  
113
val pp_prog_type : Format.formatter -> program -> unit
113
val pp_prog_type : Format.formatter -> program_t -> unit
114 114

  
115
val pp_prog_clock : Format.formatter -> program -> unit
115
val pp_prog_clock : Format.formatter -> program_t -> unit
116 116

  
117 117
val const_of_top: top_decl -> const_desc
118 118
val node_of_top: top_decl -> node_desc
......
120 120
val typedef_of_top: top_decl -> typedef_desc
121 121
val dependency_of_top: top_decl -> (bool * ident)
122 122

  
123
val get_nodes : program -> top_decl list
124
val get_imported_nodes : program -> top_decl list
125
val get_consts : program -> top_decl list
126
val get_typedefs: program -> top_decl list
127
val get_dependencies : program -> top_decl list
128
(* val prog_unfold_consts: program -> program *)
123
val get_nodes : program_t -> top_decl list
124
val get_imported_nodes : program_t -> top_decl list
125
val get_consts : program_t -> top_decl list
126
val get_typedefs: program_t -> top_decl list
127
val get_dependencies : program_t -> top_decl list
128
(* val prog_unfold_consts: program_t -> program_t *)
129 129

  
130 130
val rename_static: (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_desc
131 131
val rename_carrier: (ident -> ident) -> clock_dec_desc -> clock_dec_desc
......
142 142
(** val rename_aut f_node f_var aut *)
143 143
val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc
144 144
(** rename_prog f_node f_var prog *)
145
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
145
val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program_t -> program_t
146 146

  
147 147
val substitute_expr: var_decl list -> eq list -> expr -> expr
148 148

  
src/lustreSpec.ml
211 211
     top_decl_itf: bool;                (* header or source file ? *)
212 212
     top_decl_loc: Location.t}          (* the location where it is defined *)
213 213

  
214
type program = top_decl list
214
type program_t = top_decl list
215 215

  
216 216
type dep_t = Dep of
217 217
    bool
src/main_lustre_compiler.ml
71 71
    else
72 72
      prog
73 73
  in
74
  let params = Backends.get_normalization_params () in
75

  
74 76
  let prog, dependencies = 
75 77
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
76 78
    try 
77
      Compiler_stages.stage1 prog dirname basename
79
      Compiler_stages.stage1 params prog dirname basename
78 80
    with Compiler_stages.StopPhase1 prog -> (
79 81
      if !Options.lusi then
80 82
	begin
src/main_lustre_testgen.ml
45 45

  
46 46
  (* Parsing source *)
47 47
  let prog = parse_source source_name in
48
  let prog, dependencies = Compiler_stages.stage1 prog dirname basename in
48
  let params = Backends.get_normalization_params () in
49
  let prog, dependencies = Compiler_stages.stage1 params prog dirname basename in
49 50

  
50 51
  (* Two cases
51 52
     - generation of coverage conditions
......
73 74
       (2) produced as EMF
74 75
    *)
75 76
    Options.output := "emf";
76
    let prog_mcdc = Normalization.normalize_prog ~backend:"emf" prog_mcdc in
77
    let params = Backends.get_normalization_params () in
78
    let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
77 79
    let machine_code = Compiler_stages.stage2 prog_mcdc in
78 80
    let source_emf = source_file ^ ".emf" in 
79 81
    let source_out = open_out source_emf in
src/main_lustre_verifier.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 Format
13
open Log
14
open Compiler_common
15

  
16
open Utils
17
open LustreSpec
18
 
19

  
20
let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m"
21

  
22
let extensions = [".ec"; ".lus"; ".lusi"]
23

  
24

  
25
(* verify a .lus source file 
26

  
27
we have multiple "backends"
28
- zustre: linked to z3/spacer. Shall preserve the structure and rely on contracts. Produces both a lustre model with new properties, maybe as a lusi with lustre contract, and a JSON summarizing the results and providing tests cases or counter examples if any
29

  
30
- seal: linked to seal. Require global inline and main node
31
  focuses only on the selected node (the main)
32
  map the machine code into SEAL datastructure and compute invariants
33
  - provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content)
34
  - simplification of program through taylor expansion
35
  - scaling when provided with typical ranges (not required to be sound for the moment)
36
  - computation of lyapunov invariants
37
  - returns an annotated node with invariants and a JSON to explain computation
38
  - could also returns plots
39

  
40
- tiny: linked to tiny library to perform floating point analyses
41
  shall be provided with ranges for inputs or local variables (memories)
42
  
43
*)
44
let rec verify dirname basename extension =
45
  let source_name = dirname ^ "/" ^ basename ^ extension in
46

  
47
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
48

  
49
  (* Parsing source *)
50
  let prog = parse_source source_name in
51

  
52
  (* Checking which solver is active *)
53
  let verifier = Verifiers.get_active () in
54
  let module Verifier = (val verifier : VerifierType.S) in
55

  
56
  
57
  (* Normalizing it *)
58
  let prog, dependencies = 
59
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
60
    try
61
      let params = Verifier.get_normalization_params () in
62
      Compiler_stages.stage1 params prog dirname basename
63
    with Compiler_stages.StopPhase1 prog -> (
64
        assert false
65
    )
66
  in
67
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
68
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
69

  
70
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
71

  
72
  let machine_code = 
73
    Compiler_stages.stage2 prog 
74
  in
75

  
76
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
77
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code.pp_machines machine_code);
78

  
79
  if Scopes.Plugin.show_scopes () then
80
    begin
81
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
82
      (* Printing scopes *)
83
      if !Options.verbose_level >= 1 then
84
	Format.printf "Possible scopes are:@   ";
85
      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
86
      exit 0
87
	
88
    end;
89

  
90
  let machine_code = Plugins.refine_machine_code prog machine_code in
91

  
92
  assert (dependencies = []); (* Do not handle deps yet *)
93
  Verifier.run basename prog machine_code;
94
  begin
95
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
96
    (* We stop the process here *)
97
    exit 0
98
  end
99

  
100

  
101
let anonymous filename =
102
  let ok_ext, ext = List.fold_left
103
    (fun (ok, ext) ext' ->
104
      if not ok && Filename.check_suffix filename ext' then
105
	true, ext'
106
      else
107
	ok, ext)
108
    (false, "") extensions in
109
  if ok_ext then
110
    let dirname = Filename.dirname filename in
111
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
112
    verify dirname basename ext
113
  else
114
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
115

  
116
let _ =
117
  Global.initialize ();
118
  Corelang.add_internal_funs ();
119
  try
120
    Printexc.record_backtrace true;
121

  
122
    let options = Options_management.lustrev_options @ (Verifiers.options ()) in
123
    
124
    Arg.parse options anonymous usage
125
  with
126
  | Parse.Error _
127
  | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
128
  | Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind)
129
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
130
  | Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1
131
  | exc -> (track_exception (); raise exc) 
132

  
133
(* Local Variables: *)
134
(* compile-command:"make -C .." *)
135
(* End: *)
src/normalization.ml
29 29
      definitions.
30 30
*)
31 31

  
32
(* Two global variables *)
33
let unfold_arrow_active = ref true
34
let force_alias_ite = ref false
35
let force_alias_internal_fun = ref false
32
type param_t =
33
  {
34
    unfold_arrow_active: bool;
35
    force_alias_ite: bool;
36
    force_alias_internal_fun: bool;
37
  }
38

  
39
let params = ref
40
               {
41
                 unfold_arrow_active = false;
42
                 force_alias_ite = false;
43
                 force_alias_internal_fun =false;
44
               }
36 45

  
37 46
  
38 47
let expr_true loc ck =
......
230 239
     in
231 240
     defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
232 241
  | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
233
      && not (!force_alias_internal_fun || alias_basic) ->
242
      && not (!params.force_alias_internal_fun || alias_basic) ->
234 243
     let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
235 244
     defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
236 245
  | Expr_appl (id, args, r) ->
......
248 257
       let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
249 258
       normalize_expr ~alias:alias node offsets defvars norm_expr
250 259
     else
251
       mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic
260
       mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
252 261
				    || not (Basic_library.is_expr_internal_fun expr)))
253 262
	 node defvars norm_expr
254
  | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
263
  | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
255 264
     (* Here we differ from Colaco paper: arrows are pushed to the top *)
256 265
     normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
257 266
  | Expr_arrow (e1,e2) ->
......
328 337
  | Expr_merge (c, hl) ->
329 338
     let defvars, norm_hl = normalize_branches node offsets defvars hl in
330 339
     defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
331
  | _ when !force_alias_ite ->
340
  | _ when !params.force_alias_ite ->
332 341
     (* Forcing alias creation for then/else expressions *)
333 342
     let defvars, norm_expr =
334 343
       normalize_expr ~alias:alias node offsets defvars expr
......
506 515
    decl'
507 516
  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
508 517

  
509
let normalize_prog ?(backend="C") decls =
510
  let old_unfold_arrow_active = !unfold_arrow_active in
511
  let old_force_alias_ite = !force_alias_ite in
512
  let old_force_alias_internal_fun = !force_alias_internal_fun in
513
  
518
let normalize_prog p decls =
514 519
  (* Backend specific configurations for normalization *)
515
  let _ =
516
    match backend with
517
    | "lustre" ->
518
    (* Special treatment of arrows in lustre backend. We want to keep them *)
519
       unfold_arrow_active := false;
520
    | "emf" -> (
521
       (* Forcing ite normalization *)
522
      force_alias_ite := true;
523
      force_alias_internal_fun := true;
524
    )
525
    | _ -> () (* No fancy options for other backends *)
526
  in
520
  params := p;
527 521

  
528 522
  (* Main algorithm: iterates over nodes *)
529
  let res = List.map normalize_decl decls in
530
  
531
  (* Restoring previous settings *)
532
  unfold_arrow_active := old_unfold_arrow_active;
533
  force_alias_ite := old_force_alias_ite;
534
  force_alias_internal_fun := old_force_alias_internal_fun;
535
  res
536
  
537
  (* Local Variables: *)
538
(* compile-command:"make -C .." *)
539
(* End: *)
523
  List.map normalize_decl decls
524

  
525
    
526
           (* Local Variables: *)
527
           (* compile-command:"make -C .." *)
528
           (* End: *)
529
    
src/options_management.ml
135 135
    "-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
136 136
  ]
137 137

  
138
let lustrev_options =
139
   common_options @
140
  [ 
141
   "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
142
    "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
143
]
144

  
145
  
138 146
let plugin_opt (name, activate, options) =
139 147
  ( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
140 148
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
141 149
 
150
let verifier_opt (name, activate, options) =
151
  ( "-" ^ name , Arg.Unit activate, "run verifier " ^ name ) ::
152
    (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
142 153

  
143 154
let get_witness_dir filename =
144 155
  (* Make sure the directory exists *)
src/pluginList.ml.in
1 1
let plugins =
2 2
  [
3
    (module Scopes.Plugin : PluginType.PluginType);
3
    (module Scopes.Plugin : PluginType.S);
4 4
    @SALSA@
5 5
  ]
src/pluginType.ml
1
module type PluginType =
1
module type S =
2 2
sig
3 3
  val name: string
4 4
  val activate: unit -> unit
src/plugins.ml
7 7
  List.flatten (
8 8
    List.map Options_management.plugin_opt (
9 9
      List.map (fun m ->
10
	let module M = (val m : PluginType.PluginType) in
10
	let module M = (val m : PluginType.S) in
11 11
	(M.name, M.activate, M.options)
12 12
      ) plugins
13 13
    ))
14 14

  
15 15
let check_force_stateful () =
16 16
  List.exists (fun m ->
17
	let module M = (val m : PluginType.PluginType) in
17
	let module M = (val m : PluginType.S) in
18 18
	M.check_force_stateful ()
19 19
  ) plugins
20 20

  
21 21
let refine_machine_code prog machine_code =
22 22
  List.fold_left (fun accu m ->
23
    let module M = (val m : PluginType.PluginType) in
23
    let module M = (val m : PluginType.S) in
24 24
    M.refine_machine_code prog accu
25 25
  ) machine_code plugins
26 26

  
27 27

  
28 28
let c_backend_main_loop_body_prefix basename mname fmt () = 
29
  List.iter (fun (m: (module PluginType.PluginType)) -> 
30
    let module M = (val m : PluginType.PluginType) in
29
  List.iter (fun (m: (module PluginType.S)) -> 
30
    let module M = (val m : PluginType.S) in
31 31
    M.c_backend_main_loop_body_prefix basename mname fmt ()) plugins
32 32

  
33 33
let c_backend_main_loop_body_suffix fmt () = 
34
  List.iter (fun (m: (module PluginType.PluginType)) -> 
35
    let module M = (val m : PluginType.PluginType) in
34
  List.iter (fun (m: (module PluginType.S)) -> 
35
    let module M = (val m : PluginType.S) in
36 36
    M.c_backend_main_loop_body_suffix fmt ()) plugins
37 37

  
38 38
(* Specific treatment of annotations when inlining, specific of declared plugins *)
src/plugins/salsa/salsa_plugin.ml
39 39
      machine_code
40 40
  
41 41
  
42
 end: PluginType.PluginType)
42
 end: PluginType.S)
src/plugins/scopes/scopes.ml
239 239

  
240 240
module Plugin : (
241 241
  sig
242
    include PluginType.PluginType
242
    include PluginType.S
243 243
    val show_scopes: unit -> bool
244 244
    end) =
245 245
struct
src/tools/seal_verifier.ml
1
let active = ref false
2

  
3
module Verifier =
4
  (struct
5
    include VerifierType.Default
6
    let name = "seal"
7
    let options = []
8
    let activate () = active := true
9
    let is_active () = !active
10
    let run basename prog machines = ()
11
                    
12
  end: VerifierType.S)
13
    
src/tools/stateflow/semantics/cPS_lustre_generator.ml
321 321
    in tr 
322 322
    
323 323
  let mkcomponent :
324
  type c. c call_t -> c -> t -> LustreSpec.program =
324
  type c. c call_t -> c -> t -> LustreSpec.program_t =
325 325
    fun call args ->
326 326
      fun tr ->
327 327
	reset_loc ();
src/tools/stateflow/semantics/cPS_transformer.ml
78 78
  val eval_act : (module ThetaType with type t = t) -> act_t -> t
79 79
  val eval_cond : cond_t -> t -> t -> t
80 80
  (* val mktransformer : t -> unit *)
81
  val mkprincipal : t -> LustreSpec.program
82
  val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program
81
  val mkprincipal : t -> LustreSpec.program_t
82
  val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program_t
83 83
end
84 84

  
85 85
module type ComparableTransformerType =
src/tools/stateflow/sf_sem.ml
80 80
     let auto_out = open_out auto_file in
81 81
     let auto_fmt = Format.formatter_of_out_channel auto_out in
82 82
     Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
83
     
84
     let prog, deps = Compiler_stages.stage1 prog "" "" in
83

  
84
     let params = Backends.get_normalization_params () in
85
     let prog, deps = Compiler_stages.stage1 params prog "" "" in
85 86

  
86 87
     Format.printf "%a@." Printers.pp_prog prog;
87 88
     let noauto_file = "sf_gen_test_noauto.lus" in (* Could be changed *)
src/tools/zustre_verifier.ml
1
open LustreSpec
2
open Machine_code
3
open Format
4
open Horn_backend_common
5
open Horn_backend
6
   
7
let active = ref false
8
let ctx = ref (Z3.mk_context [])
9

  
10
let bool_sort = Z3.Boolean.mk_sort !ctx
11
let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
12
let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
13

  
14
let const_sorts = Hashtbl.create 13
15
let get_const_sort ty_name =
16
  Hashtbl.find const_sorts ty_name
17

  
18
let decl_sorts () =
19
  Hashtbl.iter (fun typ decl ->
20
    match typ with
21
    | Tydec_const var ->
22
      (match decl.top_decl_desc with
23
      | TypeDef tdef -> (
24
	match tdef.tydef_desc with
25
	| Tydec_enum tl ->
26
	  let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
27
          Hashtbl.add const_sorts var new_sort
28
	| _ -> assert false
29
      )
30
      | _ -> assert false
31
      )
32
    | _        -> ()) Corelang.type_table
33

  
34

  
35
let rec type_to_sort t =
36
  if Types.is_bool_type t  then bool_sort else
37
    if Types.is_int_type t then int_sort else 
38
  if Types.is_real_type t then real_sort else 
39
  match (Types.repr t).Types.tdesc with
40
  | Types.Tconst ty       -> get_const_sort ty
41
  | Types.Tclock t        -> type_to_sort t
42
  | Types.Tarray(dim,ty)   -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
43
  | Types.Tstatic(d, ty)-> type_to_sort ty
44
  | Types.Tarrow _
45
  | _                     -> Format.eprintf "internal error: pp_type %a@."
46
                               Types.print_ty t; assert false
47

  
48
  
49
let decl_var id =
50
  Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)
51

  
52
let decl_machine machines m =
53
  if m.Machine_code.mname.node_id = Machine_code.arrow_id then
54
    (* We don't print arrow function *)
55
    ()
56
  else
57
    begin
58
      let _ = List.map decl_var 
59
      	(
60
	  (inout_vars machines m)@
61
	    (rename_current_list (full_memory_vars machines m)) @
62
	    (rename_mid_list (full_memory_vars machines m)) @
63
	    (rename_next_list (full_memory_vars machines m)) @
64
	    (rename_machine_list m.mname.node_id m.mstep.step_locals)
65
	)
66
      in
67
      ()
68
     (*
69
      if is_stateless m then
70
	begin
71
	  (* Declaring single predicate *)
72
	  fprintf fmt "(declare-rel %a (%a))@."
73
	    pp_machine_stateless_name m.mname.node_id
74
	    (Utils.fprintf_list ~sep:" " pp_type)
75
	    (List.map (fun v -> v.var_type) (inout_vars machines m));
76

  
77
          match m.mstep.step_asserts with
78
	  | [] ->
79
	     begin
80

  
81
	       (* Rule for single predicate *)
82
	       fprintf fmt "; Stateless step rule @.";
83
	       fprintf fmt "@[<v 2>(rule (=> @ ";
84
	       ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) )  m fmt m.mstep.step_instrs);
85
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
86
		 pp_machine_stateless_name m.mname.node_id
87
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
88
	     end
89
	  | assertsl ->
90
	     begin
91
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
92
	       
93
	       fprintf fmt "; Stateless step rule with Assertions @.";
94
	       (*Rule for step*)
95
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
96
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
97
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
98
		 pp_machine_stateless_name m.mname.node_id
99
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
100
	  
101
	     end
102
	       
103
	end
104
      else
105
	begin
106
	  (* Declaring predicate *)
107
	  fprintf fmt "(declare-rel %a (%a))@."
108
	    pp_machine_reset_name m.mname.node_id
109
	    (Utils.fprintf_list ~sep:" " pp_type)
110
	    (List.map (fun v -> v.var_type) (reset_vars machines m));
111

  
112
	  fprintf fmt "(declare-rel %a (%a))@."
113
	    pp_machine_step_name m.mname.node_id
114
	    (Utils.fprintf_list ~sep:" " pp_type)
115
	    (List.map (fun v -> v.var_type) (step_vars machines m));
116

  
117
	  pp_print_newline fmt ();
118

  
119
	  (* Rule for reset *)
120
	  fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
121
	    (pp_machine_reset machines) m 
122
	    pp_machine_reset_name m.mname.node_id
123
	    (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
124

  
125
          match m.mstep.step_asserts with
126
	  | [] ->
127
	     begin
128
	       fprintf fmt "; Step rule @.";
129
	       (* Rule for step*)
130
	       fprintf fmt "@[<v 2>(rule (=> @ ";
131
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
132
	       fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
133
		 pp_machine_step_name m.mname.node_id
134
		 (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
135
	     end
136
	  | assertsl -> 
137
	     begin
138
	       let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
139
	       (* print_string pp_val; *)
140
	       fprintf fmt "; Step rule with Assertions @.";
141
	       
142
	       (*Rule for step*)
143
	       fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
144
	       ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
145
	       fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
146
		 pp_machine_step_name m.mname.node_id
147
		 (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
148
	     end
149
	       
150
     	       
151
	end
152
      *)  end
153

  
154
           
155
module Verifier =
156
  (struct
157
    include VerifierType.Default
158
    let name = "zustre"
159
    let options = []
160
    let activate () = (
161
        active := true;
162
        Options.output := "horn";
163
      )
164
    let is_active () = !active
165

  
166
    let get_normalization_params () =
167
      (* make sure the output is "Horn" *)
168
      assert(!Options.output = "horn");
169
      Backends.get_normalization_params ()
170

  
171
    let run basename prog machines =
172
      let machines = Machine_code.arrow_machine::machines in
173
      let machines = preprocess machines in
174
      decl_sorts ();
175
      List.iter (decl_machine machines) (List.rev machines);
176

  
177
      
178
      ()
179

  
180
  end: VerifierType.S)
181
    
src/verifierList.ml.in
1
let verifiers =
2
  [
3
    @LUSTREV_SEAL@
4
    @LUSTREV_ZUSTRE@
5
    @LUSTREV_TINY@
6
  ]
src/verifierType.ml
1
module type S =
2
sig
3
  val name: string
4
  val activate: unit -> unit
5
  val is_active: unit -> bool
6
  val options: (string * Arg.spec * string) list
7
  val get_normalization_params: unit -> Normalization.param_t
8
  val run: string -> LustreSpec.program_t -> Machine_code.machine_t list -> unit 
9
end
10

  
11
module Default =
12
  struct
13

  
14
    let get_normalization_params () = {
15
    Normalization.unfold_arrow_active = true;
16
    force_alias_ite = false;
17
    force_alias_internal_fun = false;
18
  }
19

  
20
  end
src/verifiers.ml
1
open LustreSpec
2

  
3
open VerifierList
4

  
5
let active = ref None
6
           
7
let options () = 
8
  List.flatten (
9
    List.map Options_management.verifier_opt (
10
      List.map (fun m ->
11
	let module M = (val m : VerifierType.S) in
12
	(M.name, M.activate, M.options)
13
      ) verifiers
14
    ))
15
  
16
let verifier_list verifiers =
17
  List.fold_left (fun acc m ->
18
      let module M =  (val m : VerifierType.S) in
19
      (if acc = "" then "" else acc ^ ", ") ^ M.name
20
    ) "" verifiers
21
  
22
let get_active () =
23
  match !active with
24
  | None ->
25
     begin
26
       (* check that a single one is active and register it *)
27
       let found =
28
         List.fold_left (fun found m ->
29
             let module M =  (val m : VerifierType.S) in
30
             if M.is_active () then
31
               m::found
32
             else
33
               found
34
           ) [] verifiers
35
       in
36
       match found with
37
       | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers))
38
       | [m] -> active := Some m; m
39
       | _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found))
40
     end
41

  
42
  | Some m -> m
43

  
44

  
45
                
46
                (* Local Variables: *)
47
                (* compile-command:"make -C .." *)
48
                (* End: *)

Also available in: Unified diff