Project

General

Profile

Revision 9b0432bc

View differences:

.ocamlformat
1
profile = ocamlformat
2
break-cases = fit
3
margin = 90
4
parse-docstrings = true
5
wrap-comments = true
README.md
125 125
```
126 126
# frama-c -cpp-extra-args='-Iinclude'  filename.c
127 127
```
128
#### Tiny backend
129

  
130
The Tiny backend generates tiny (imperative) code from lustre. 
131
The example below generates tiny code for the node top of the two_counters.lus file
132

  
133
```
134
lustrec -d examples/two_counters -tiny -node top examples/two_counters/two_counters.lus
135
```
136

  
137
### Lustrev 
138

  
139
Lustrev is a Lustre verifier based on static analysis. 
140

  
141
#### Tiny verifier
142

  
143
With the option `-tiny` the verifier uses Tiny to analyse Lustre file. Tiny is based on theory of abstract interpretation. Set of values are represented as abstract values that overapproximate the values that can be taken by a variable.
144

  
145
This verifier runs an abstract simulation of the Lustre code. At each time step, the verifier outputs abstract values of the variable environnement.
146

  
147
It takes an Lustre file, a top node, a JSON file with the bounds on the parameters of the top node, and outputs a JSON file consisting of the abstract values of the variables at each time step.
148

  
149
The example below generates a two_counters_tiny.json file.
150
```
151
cd examples/two_counters
152
lustrev -node top -tiny -tiny-duration 5 -tiny-bounds-file tiny_input.json -tiny-output two_counters.lus 
153
```
154

  
128 155
### Ada backend 
129 156

  
130 157
Download ada from https://www.adacore.com/download
backends/C/c_backend_makefile.ml
98 98
    fprintf fmt "BINNAME?=%s@." binname;
99 99
    fprintf fmt "GCC=gcc -O0@.";
100 100
    fprintf fmt "LUSTREC=%s@." Sys.executable_name;
101
    fprintf fmt "LUSTREC_BASE=%s@." (Filename.dirname (Filename.dirname Sys.executable_name));
102
    fprintf fmt "INC=${LUSTREC_BASE}/include/lustrec@.";
101
    fprintf fmt "INC=%s@." Lustrec.Version.include_path;
103 102
    fprintf fmt "@.";
104 103

  
105 104
    (* Main binary *)
backends/dune
9 9
(library
10 10
(wrapped false)
11 11
(name backends)
12
(libraries lustrec mpfr_plugin)
12
(libraries lustrec mpfr_plugin tiny)
13
(preprocess (staged_pps ppx_deriving_yojson ppx_import ppx_deriving.show))
13 14
(modules :standard  \
14 15
 c_backend_cmake
15 16
java_backend
backends/tiny/tiny_backend.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - ISAE-SUPAERO     *)
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 Lustrec.Machine_code_types
14
open Lustrec
15
open Misc_lustre_function
16
open Ada_printer
17
open Ada_backend_common
18
open Tiny_utils
19

  
20
let indent_size = 2
21

  
22

  
23
(** Main function of the Tiny backend. 
24
   @param basename name of the lustre file
25
   @param prog useless
26
   @param machines list of machines to translate
27
   @param dependencies useless
28
**)
29
let translate_to_tiny basename prog machines dependencies =
30
  
31
  let node_name =
32
    match !Lustrec.Options.main_node with
33
    | "" -> (
34
      Format.eprintf "Tiny backend requires a main node.@.";
35
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
36
        (Lustrec.Utils.fprintf_list ~sep:"@ "
37
            (fun fmt m ->
38
              Format.fprintf fmt "%s" m.Lustrec.Machine_code_types.mname.node_id
39
            )
40
        )
41
        machines; 
42
      exit 1
43
    )
44
    | s -> ( (* should have been addessed before *)
45
      match Lustrec.Machine_code_common.get_machine_opt machines s with
46
      | None -> begin
47
          Lustrec.Global.main_node := s;
48
          Format.eprintf "Code generation error: %a@."Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
49
          raise (Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
50
        end
51
      | Some _ -> s
52
    )
53
  in
54
  let m = Lustrec.Machine_code_common.get_machine machines node_name in
55
  let env = (* We add each variables of the node the Tiny env *)
56
    Tiny_utils.machine_to_env m in
57
  let nd = m.mname in
58
  (* Building preamble with some bounds on inputs *)
59
  (* TODO: deal woth contracts, asserts, ... *)
60
  let bounds_inputs = [] in
61
  let ast = (Tiny_utils.machine_to_tiny_encoding bounds_inputs m).ast in
62

  
63
  (* pretty print in lowercase *)  
64
  let pp_lowercase pp fmt =
65
  let str = asprintf "%t" pp in
66
  fprintf fmt "%s" (String. lowercase_ascii str) in 
67

  
68
  (* pretty print a filename with an extension *) 
69
  let pp_filename extension fmt pp_name =
70
    fprintf fmt "%t.%s" (pp_lowercase pp_name) extension in 
71

  
72
  let pp_var_decl env fmt = 
73
  let vars = Tiny_utils.Ast.VarSet.elements env in 
74
  List.iter (fun (var_name, var_type) -> 
75
    fprintf fmt "%a %s;\n" Tiny_utils.Ast.pp_base_type var_type var_name 
76
  ) vars in 
77

  
78

  
79
  let destname = !Lustrec.Options.dest_dir ^ "/" in
80

  
81
  let path = asprintf "%s%a" destname (pp_filename "tiny") (fun fmt -> fprintf fmt "%s" basename) in
82
  let out = open_out path in
83
  let fmt = formatter_of_out_channel out in
84
  pp_var_decl env fmt ;
85
  Tiny.Ast.fprint_stm fmt ast;
86
  pp_print_flush fmt ();
87
  close_out out; 
88
       
89

  
90

  
backends/tiny/tiny_utils.ml
1
open Lustrec
2
open Machine_code_types
3
open Format 
4
open Yojson
5
open Printers 
6

  
7
module Ast = Tiny.Ast
8

  
9
type bound = {
10
  var_name: string;
11
  _type: string;[@key "type"]
12
  inf: string;
13
  sup: string
14
} [@@deriving yojson]
15
type bounds = bound list [@@deriving yojson]
16

  
17

  
18
let gen_loc () = Tiny.Location.dummy ()
19
               
20
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Lustrec.Location.loc_start loc.Lustrec.Location.loc_end
21
                     
22
let tloc_to_lloc loc = assert false (*Lustrec.Location.dummy_loc (*TODO*) *)
23

  
24
(* Take a List of Ast.stm (Tiny statements) and 
25
   make an Ast Seq node from the statements *)
26
let stmt_list_to_ast (stmt_list:Ast.stm list) = 
27
  let location_last_statement = gen_loc() in
28
  let stmt_seq = List.fold_right (fun stm ast -> Ast.Seq (gen_loc(), stm, ast)) 
29
  stmt_list (Ast.Nop location_last_statement) in 
30
  stmt_seq
31

  
32
(* Take a Lustre Type and return the corresponding Tiny type *)                     
33
let ltyp_to_ttyp t =
34
  if Lustrec.Types.is_real_type t then Tiny.Ast.RealT
35
  else if Lustrec.Types.is_int_type t then Tiny.Ast.IntT
36
  else if Lustrec.Types.is_bool_type t then Tiny.Ast.BoolT
37
  else assert false (* not covered yet *)
38

  
39
(* Create a Tiny boolean constant *)
40
let cst_bool (loc:Tiny.Location.t) (b:bool) =
41
  { Ast.expr_desc =
42
      if b then
43
        Ast.Cst(Q.of_int 1, "true")
44
      else
45
        Ast.Cst(Q.of_int 0, "false");
46
    expr_loc = loc;
47
    expr_type = Ast.BoolT }
48

  
49
(* Create a Tiny numeric constant *)
50
let cst_num (loc:Tiny.Location.t) (t:Tiny.Ast.base_type) (q:Q.t) =
51
{ Ast.expr_desc =
52
    Ast.Cst(q, Q.to_string q);
53
  expr_loc = loc;
54
  expr_type = t }
55
  
56
let rec real_to_q man exp =
57
  if exp = 0 then
58
        Q.of_string (Num.string_of_num man)
59
  else
60
    if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
61
    else (* if exp<0 then *)
62
      Q.mul
63
        (real_to_q man (exp+1))
64
        (Q.of_int 10)
65

  
66
(* Take a Lustrec instruction and return a Tiny location *)
67
let instr_loc i =
68
  match i.Lustrec.Machine_code_types.lustre_eq with
69
  | None -> gen_loc ()
70
  | Some eq -> lloc_to_tloc eq.eq_loc
71
             
72
(* Convert a lustrec value to a Tiny expression *)
73
let rec lval_to_texpr loc _val =
74
  let build d v =
75
      Ast.{ expr_desc = d;
76
            expr_loc = gen_loc ();
77
            expr_type = v }
78
  in
79
  let new_desc =
80
    match _val.Lustrec.Machine_code_types.value_desc with
81
  | Lustrec.Machine_code_types.Cst cst -> (
82
    match cst with
83
      Lustrec.Lustre_types.Const_int n -> Ast.Cst (Q.of_int n, string_of_int n)
84
    | Const_real r -> Ast.Cst (Lustrec.Real.to_q r, Lustrec.Real.to_string r) 
85
  | Const_array _ -> failwith "Const_array not yet supported"
86
  | Const_tag id -> (match id with 
87
    | "true" ->  Ast.Cst(Q.of_int 1,id) 
88
    | "false" -> Ast.Cst(Q.of_int 0, id)
89
    |_ -> failwith ("Const_tag "^ id^" not yet supported"))
90
  | Const_string _ -> failwith "Const_string not yet suported"
91
  | Const_modeid _ -> failwith "Const_modeid not yet supported"
92
  | Const_struct _ -> failwith "Const_struct not yet supported"
93
      | _ -> assert false
94
  )
95
     
96
  | Var v -> Ast.Var (v.var_id)
97
  | Fun (op, vl) ->
98
     let t_arg = match vl with
99
       | hd::_ -> ltyp_to_ttyp hd.value_type
100
       | _ -> assert false
101
     in
102
     (
103
       match op, List.map (lval_to_texpr loc) vl with
104
       | "+", [v1;v2] -> Ast.Binop (Ast.Plus, v1, v2)
105
       | "-", [v1;v2] -> Ast.Binop (Ast.Minus, v1, v2)
106
       | "*", [v1;v2] -> Ast.Binop (Ast.Times, v1, v2)
107
       | "/", [v1;v2] -> Ast.Binop (Ast.Div, v1, v2)
108
       | "<", [v1;v2] ->
109
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Strict)
110
       | "<=", [v1;v2] ->
111
          Ast.Cond (build(Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Loose)
112
       | ">", [v1;v2] ->
113
          Ast.Cond (build(Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Strict)
114
       | ">=", [v1;v2] ->
115
          Ast.Cond (build (Ast.Binop (Ast.Minus, v1, v2)) t_arg, Ast.Loose)
116
       | "=", [v1;v2] ->
117
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
118
       | "equi", [v1;v2] ->
119
          (* generate an ast node based on 
120
            v1 <=> v2 if and only if v1 && v2 || (!v1 &&!v2) *)
121
          let tt = build (Ast.Binop (Ast.And,v1,v2)) BoolT and
122
           ff = build (Ast.Binop (Ast.And,(build (Ast.Unop (Ast.Not, v1)) BoolT),(build (Ast.Unop (Ast.Not, v2)) BoolT))) BoolT in
123
          Ast.Binop (Ast.Or, tt, ff)
124
       | "!=", [v1;v2] ->
125
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
126
       | "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1)
127
       | "not", [v1] -> Ast.Unop (Ast.Not, v1)
128
       | "&&", [v1;v2] -> Ast.Binop (Ast.And, v1, v2)
129
       | "||", [v1;v2] -> Ast.Binop (Ast.Or, v1, v2)
130
       | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
131
  )
132
  | Array vl      -> failwith "array are not supported yet"
133
  | Access (t, i) -> failwith "acces not supported yet"
134
  | Power (v, n)  -> failwith "powser not supported yet"
135
  | _ -> assert false (* no array. access or power *)
136
  in
137
  build new_desc (ltyp_to_ttyp _val.value_type)
138

  
139
  
140
let machine_body_to_ast init m =
141
  let init_var = ref None in
142
  let rec guarded_expr_to_stm loc te guarded_instrs =
143
    match guarded_instrs with
144
    | [] -> assert false
145
    | [_,il] -> instrl_to_stm il
146
    | (label, il)::tl ->
147
       let stmt = instrl_to_stm il in
148
       let guard= match label with
149
           "true" -> te
150
         | "false" -> Ast.neg_guard te
151
         | _ -> assert false (* TODO: don't deal with non boolean
152
                                guards. Could just treturn true and
153
                                over-approximate behavior *)
154
       in
155
       if (match !init_var, te.Ast.expr_desc with
156
           | Some v, Var v2 -> v = v2
157
           | _ -> false) then 
158
         instrl_to_stm (
159
             if init then
160
               (List.assoc "true" guarded_instrs)
161
             else
162
               (List.assoc "false" guarded_instrs)
163
           )
164
       else
165
         Ast.Ite (loc, guard, stmt, guarded_expr_to_stm loc te tl)
166
  and instr_to_stm i =
167
    let loc = instr_loc i in
168
    match i.instr_desc with
169
    | MLocalAssign (v, e) | MStateAssign (v, e) ->
170
       Ast.Asn (loc, v.var_id, (lval_to_texpr loc) e)
171
    | MBranch (e, guarded_instrs) -> (
172
      let te = lval_to_texpr loc e in
173
      guarded_expr_to_stm loc te guarded_instrs
174
    )
175
    | MStep (ol, id, args) ->
176
       if List.mem_assoc id m.Lustrec.Machine_code_types.minstances then
177
         let fun_name, _ = List.assoc id m.minstances in
178
         match Lustrec.Corelang.node_name fun_name, ol with
179
         | "_arrow", [o] -> (
180
           init_var := Some o.var_id;
181
           Ast.Nop (loc);
182
             (* Ast.Asn (loc, o.var_id, 
183
              *        { expr_desc =              if init then Ast.Cst(Q.of_int 1, "true") else Ast.Cst(Q.of_int 0, "false");
184
              *          expr_loc = loc;
185
              *          expr_type = Ast.BoolT }
186
              * ) *)
187
         )
188
         | name, _ -> 
189
            (
190
              Format.eprintf "No tiny translation for node call  %s@.@?" name;
191
              assert false
192
            )
193
       else (
194
         Format.eprintf "No tiny translation for node call  %s@.@?" id;
195
         assert false
196
       )
197
    | MReset id
198
    | MNoReset id -> assert false (* no more calls or functions, ie. no reset *)
199
    | MComment s 
200
      | MSpec s -> assert false
201
  and instrl_to_stm il =
202
    match il with
203
      [] -> assert false
204
    | [i] -> instr_to_stm i
205
    | i::il ->
206
       let i' = instr_to_stm i in
207
       Ast.Seq (gen_loc (), i', (instrl_to_stm il))
208
  in
209
  let stmts_print_output =  List.map (fun (o:Lustre_types.var_decl)-> 
210
    let ast_variable =  Ast.{ expr_desc = Ast.Var(o.var_id);
211
            expr_loc = gen_loc ();
212
            expr_type =ltyp_to_ttyp o.var_type } in 
213
    (* printing_function_name = print_{bool/int/real} depending on the type of the variable *)
214
    let printing_function_name = (Format.asprintf "print_%a" Ast.pp_base_type (ltyp_to_ttyp o.var_type)) in 
215
     Ast.Asn (gen_loc(), "_ignore", 
216
        Ast.{ expr_desc = Ast.Call(printing_function_name ,[ast_variable]);
217
            expr_loc = gen_loc ();
218
            expr_type = Ast.BoolT }
219
      )
220
  ) m.mname.node_outputs |> stmt_list_to_ast in
221
  let translation = instrl_to_stm m.Lustrec.Machine_code_types.mstep.step_instrs in 
222
  Ast.Seq (gen_loc (), translation,stmts_print_output)
223

  
224
 
225

  
226

  
227

  
228

  
229

  
230
let read_var bound v =
231
  (* TODO : manage boolean cases properly *)
232
  let range = {
233
      Ast.expr_desc = Ast.Rand ((Q.of_string bound.inf, bound.inf),(Q.of_string bound.sup, bound.sup));
234
      expr_loc = gen_loc ();
235
      expr_type = ltyp_to_ttyp (v.Lustrec.Lustre_types.var_type)
236
    }
237
  in
238
  Ast.Asn (gen_loc (), v.var_id, range)
239
  
240
let rec read_vars bounds_inputs vl =
241
  let find_bound_of_var v  = 
242
      (match List.find_all (fun bound -> bound.var_name = Lustrec.Lustre_types.(v.var_id)) bounds_inputs with 
243
      | [] -> begin
244
        Log.report ~level:0 (fun fmt -> fprintf fmt ".. error %a is not bound @." pp_var v);
245
        exit 2
246
      end
247
      | [b] -> b
248
      | b::bs -> begin 
249
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. warning %a is bound multiple times ignoring constraints other than the first one @." pp_var v);
250
        b
251
      end
252
    ) 
253
  in 
254
  let reading_statements = List.map (fun v -> 
255
    let bound = find_bound_of_var v in 
256
    read_var bound v
257
  ) vl 
258
  in stmt_list_to_ast reading_statements;
259
(*
260
A type to encode the Lustre machine in the Tiny world
261
*)
262
type tiny_encoding = {
263
  ast:Ast.stm; 
264
  variables: Ast.VarSet.t; 
265
  location_beg_while: Tiny.Location.t; 
266
}
267

  
268

  
269
let machine_to_env m =
270
    let var_set = List.fold_left (fun accu v ->
271
      let typ =
272
        ltyp_to_ttyp (v.Lustrec.Lustre_types.var_type)
273
      in
274
      Ast.VarSet.add (v.var_id, typ) accu)
275
    Ast.VarSet.empty
276
    (Lustrec.Machine_code_common.machine_vars m ) in 
277
    (* adding a dummy variable for printing functions *)
278
    Ast.VarSet.add ("_ignore", BoolT) var_set
279

  
280
    
281
let machine_to_tiny_encoding bounds_input m = (
282
  let read_vars = read_vars bounds_input m.Lustrec.Machine_code_types.mstep.step_inputs in
283
  Log.report ~level:5 (fun fmt -> fprintf fmt ".. raw machine code %s@ " (show_machine_t m));
284
  let ast_loop_first = machine_body_to_ast true m in
285
  let ast_loop_run = machine_body_to_ast false m in
286
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
287
  let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
288
  {
289
    ast= Ast.Seq (gen_loc (), read_vars, (Ast.Seq (gen_loc (), ast_loop_first, loop)));
290
    variables= machine_to_env m;
291
    location_beg_while = Ast.loc_of_stm ast_loop_body;
292
  }
293
)
294

  
295

  
configure.ac
10 10
fi
11 11

  
12 12
if test -z "$share"; then
13
  share="$ac_pwd/_build/default/include"
13
  share="$ac_pwd/_build/install/default/share/lustrec"
14 14
fi
15 15

  
16 16
AC_SUBST(SHARE_PATH, $share)
examples/two_counters/tiny_input.json
1
[
2
    {"var_name": "x", "type": "int", "inf": "-1", "sup": "1"}
3
]
examples/two_counters/two_counters.lus
1
-- a simple boolean ant int counter
2

  
3
node greycounter (x:int) returns (out:bool);
4
var a,b:bool;
5
let
6
  a = false -> not pre(b);
7
  b = false -> pre(a);
8
  out = a and b;
9
tel
10

  
11
node intloopcounter (x:int) returns (out:bool);
12
var time: int;
13
let
14
  time = 0 -> if pre(time) = 3 then 0
15
            else pre time + 1;
16
  out = (time = 2);
17
tel
18

  
19

  
20
node top (x:int) returns (OK:bool);
21
var b,d:bool;
22
let
23
  b = greycounter(x);
24
  d = intloopcounter(x);
25
  OK = b = d;
26
tel
lib/backends.ml
3 3

  
4 4
let setup () =
5 5
  match !Options.output with
6
  | "tiny" -> begin
7
    Options.global_inline := true;
8
    Options.optimization := 0;
9
    Options.const_unfold := true;
10
  end
11

  
6 12
  | "emf" ->
7 13
     (* Not merging branches *)
8 14
     join_guards := false;
lib/clocks.ml
33 33
    {mutable carrier_desc: carrier_desc;
34 34
     mutable carrier_scoped: bool;
35 35
     carrier_id: int}
36
[@@deriving show]
36 37
     
37 38
type clock_expr =
38 39
    {mutable cdesc: clock_desc;
......
41 42

  
42 43
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
43 44
and clock_desc =
44
  | Carrow of clock_expr * clock_expr
45
  | Ctuple of clock_expr list
45
  | Carrow of clock_expr * clock_expr (* clock of a node *)
46
  | Ctuple of clock_expr list (* clock of a tuple expression *)
46 47
  | Con of clock_expr * carrier_expr * ident
47 48
  (* | Pck_up of clock_expr * int *)
48 49
  (* | Pck_down of clock_expr * int *)
......
52 53
  | Cunivar (* of clock_set *) (* Polymorphic clock variable *)
53 54
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
54 55
  | Ccarrying of carrier_expr * clock_expr
55

  
56
[@@deriving show]
56 57
type error =
57 58
  | Clock_clash of clock_expr * clock_expr
58 59
  (* | Not_pck *)
lib/delay.ml
24 24
  | Dtuple of delay_expr list
25 25
  | Dlink of delay_expr (* During unification, make links instead of substitutions *)
26 26
  | Dunivar (* Polymorphic type variable *)
27
[@@deriving show]
28

  
27 29
type error =
28 30
  | Delay_clash of delay_expr * delay_expr
29 31

  
lib/dimension.ml
25 25
| Dlink of dim_expr
26 26
| Dvar
27 27
| Dunivar
28
[@@deriving show]
29

  
28 30

  
29 31
exception Unify of dim_expr * dim_expr
30 32
exception InvalidDimension
lib/dune
9 9
(library
10 10
(name lustrec)
11 11
(libraries unix dune-build-info ocamlgraph str zarith num)
12
(preprocess (pps ppx_import ppx_deriving.show))
12 13
)
lib/location.ml
9 9
(*                                                                  *)
10 10
(********************************************************************)
11 11

  
12
type t = { loc_start: Lexing.position; loc_end: Lexing.position }
12
type position = [%import: Lexing.position] [@@deriving show]
13

  
14
type t = { loc_start: Lexing.position [@printer pp_position]; loc_end: Lexing.position [@printer pp_position]}
15
[@@deriving show]
13 16

  
14 17
type filename = string
18
[@@deriving show]
15 19

  
16 20
let dummy_loc = {loc_start=Lexing.dummy_pos; loc_end=Lexing.dummy_pos}
17 21

  
lib/lustre_types.ml
11 11

  
12 12

  
13 13
type ident = Utils.ident
14
[@@deriving show]
14 15
type rat = Utils.rat
16
[@@deriving show]
15 17
type tag = Utils.tag
18
[@@deriving show]
16 19
type label = Utils.ident
20
[@@deriving show]
17 21

  
18 22
type type_dec =
19 23
    {ty_dec_desc: type_dec_desc;
......
30 34
  | Tydec_enum of ident list
31 35
  | Tydec_struct of (ident * type_dec_desc) list
32 36
  | Tydec_array of Dimension.dim_expr * type_dec_desc
37
[@@deriving show]
33 38

  
34 39
type typedec_desc =
35 40
    {tydec_id: ident}
41
 [@@deriving show]
36 42

  
37 43
type typedef_desc =
38 44
    {tydef_id: ident;
39 45
     tydef_desc: type_dec_desc}
46
 [@@deriving show]
40 47

  
41 48
type clock_dec =
42 49
    {ck_dec_desc: clock_dec_desc;
......
45 52
and clock_dec_desc =
46 53
  | Ckdec_any
47 54
  | Ckdec_bool of (ident * ident) list
48

  
55
 [@@deriving show]
49 56

  
50 57
type constant =
51 58
  | Const_int of int
......
55 62
  | Const_string of string (* used only for annotations *)
56 63
  | Const_modeid of string (* used only for annotations *)
57 64
  | Const_struct of (label * constant) list
65
 [@@deriving show]
58 66

  
59 67
type quantifier_type = Exists | Forall
68
[@@deriving show]
60 69

  
61 70
type var_decl =
62 71
    {var_id: ident;
......
126 135
and expr_annot =
127 136
 {annots: (string list * eexpr) list;
128 137
  annot_loc: Location.t}
138
[@@deriving show]
129 139

  
130 140
type contract_mode =
131 141
  {
......
134 144
    ensure: eexpr list;
135 145
    mode_loc: Location.t
136 146
  }
147
 [@@deriving show]
137 148

  
138 149
type contract_import =
139 150
  { import_nodeid: ident;
140 151
    inputs: expr;
141 152
    outputs: expr;
142 153
    import_loc: Location.t }
143
    
154
  [@@deriving show]  
144 155

  
145 156

  
146 157
type offset =
147 158
| Index of Dimension.dim_expr
148 159
| Field of label
160
 [@@deriving show]
149 161

  
150 162
type assert_t =
151 163
    {
152 164
      assert_expr: expr;
153 165
      assert_loc: Location.t;
154 166
    }
167
[@@deriving show]
155 168

  
156 169
type statement =
157 170
| Eq of eq
......
171 184
   hand_asserts: assert_t list;
172 185
   hand_annots: expr_annot list;
173 186
   hand_loc: Location.t}
187
[@@deriving show]
174 188

  
175 189
type contract_desc = 
176 190
  {
......
183 197
    imports: contract_import list; 
184 198
    spec_loc: Location.t;
185 199
  }
200
[@@deriving show]
186 201

  
187 202
type node_spec_t = Contract of contract_desc
188 203
                 | NodeSpec of ident
204
[@@deriving show]
189 205

  
190 206
type node_desc =
191 207
    {node_id: ident;
......
204 220
     node_annot: expr_annot list;
205 221
     node_iscontract: bool;
206 222
    }
223
[@@deriving show]
207 224

  
208 225
type imported_node_desc =
209 226
    {nodei_id: ident;
......
217 234
     nodei_prototype: string option;
218 235
     nodei_in_lib: string list;
219 236
    }
237
[@@deriving show]
220 238

  
221 239
type const_desc =
222 240
    {const_id: ident;
......
224 242
     const_value: constant;
225 243
     mutable const_type: Types.type_expr;
226 244
    }
245
[@@deriving show]
227 246

  
228 247
  
229 248
type top_decl_desc =
......
235 254
  | Include of string (* the boolean set to true denotes a local
236 255
			   lus vs a lus installed at system level *)
237 256
  | TypeDef of typedef_desc
238
    
257
[@@deriving show]   
258

  
239 259
type top_decl =
240 260
    {top_decl_desc: top_decl_desc;      (* description of the symbol *)
241 261
     top_decl_owner: Location.filename; (* the module where it is defined *)
242 262
     top_decl_itf: bool;                (* header or source file ? *)
243 263
     top_decl_loc: Location.t}          (* the location where it is defined *)
264
[@@deriving show]
244 265

  
245 266
type program_t = top_decl list
267
[@@deriving show]
246 268

  
247 269
type dep_t = {
248 270
    local: bool;
......
250 272
    content: program_t;
251 273
    is_stateful: bool
252 274
  }
275
[@@deriving show]
253 276

  
254 277
type spec_types =
255 278
  | LocalContract of contract_desc
256 279
  | TopContract of top_decl list
280
[@@deriving show]
257 281

  
258 282
let tag_true = "true"
259 283
let tag_false = "false"
lib/machine_code.ml
109 109

  
110 110
let specialize_op expr =
111 111
  match !Options.output with
112
  | "C" -> specialize_to_c expr
112
  | "C" | "tiny" -> specialize_to_c expr
113 113
  | _   -> expr
114 114

  
115 115
let rec translate_expr env expr =
lib/machine_code_types.ml
14 14
  | Array of value_t list
15 15
  | Access of value_t * value_t
16 16
  | Power of value_t * value_t
17

  
17
 [@@deriving show]
18 18
type instr_t =
19 19
  {
20 20
    instr_desc: instr_t_desc; (* main data: the content *)
......
30 30
  | MBranch of value_t * (label * instr_t list) list
31 31
  | MComment of string
32 32
  | MSpec of string 
33

  
33
 [@@deriving show]
34 34
type step_t = {
35 35
    step_checks: (Location.t * value_t) list;
36 36
    step_inputs: var_decl list;
......
39 39
    step_instrs: instr_t list;
40 40
    step_asserts: value_t list;
41 41
  }
42

  
42
 [@@deriving show]
43 43
type static_call = top_decl * (Dimension.dim_expr list)
44

  
44
 [@@deriving show]
45 45
  
46 46
type machine_t = {
47 47
  mname: node_desc;
......
54 54
  mstep: step_t;
55 55
  mspec: node_spec_t option;
56 56
  mannot: expr_annot list;
57
  msch: Scheduling_type.schedule_report option; (* Equations scheduling *)
57
  msch: Scheduling_type.schedule_report option; [@opaque] (* Equations scheduling *)
58 58
}
59
[@@deriving show]
lib/options_management.ml
111 111
      "-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
112 112
      "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
113 113
      "-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";
114
      "-tiny", Arg.Unit (fun () -> set_backend "tiny"), "generates Tiny output instead of C";
114 115
      (* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *)
115 116
      "-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C";
116 117
      "-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C";
lib/parsers/parse.ml
51 51
    Parsing.clear_parser ();
52 52
    ast
53 53
  with
54
  | Parsing.Parse_error ->
54
  | Parser_lustre.Error ->
55 55
    let loc = Location.curr lexbuf in
56 56
    raise (Error (loc, Syntax_error))
57 57

  
......
61 61
    Parsing.clear_parser ();
62 62
    ast
63 63
  with
64
  | Parsing.Parse_error ->
64
  | Parser_lustre.Error ->
65 65
    let loc = Location.curr lexbuf in
66 66
    raise (Error (loc, Syntax_error))
67 67

  
lib/parsers/parser_lustre.mly
14 14
open Lustre_types
15 15
open Corelang
16 16
open Dimension
17
open Parse
18 17

  
19 18
   
20 19
let get_loc () = Location.symbol_rloc ()
lib/types.ml
43 43
    | Tbool
44 44
    | Trat (* Actually unused for now. Only place where it can appear is
45 45
              in a clock declaration *)
46
  [@@deriving show]
46 47

  
47 48
  let type_string_builder = Tstring
48 49
  let type_int_builder = Tint
......
100 101

  
101 102
  module BasicT = BasicT
102 103
  type basic_type = BasicT.t
104
  [@@deriving show]
103 105
  type type_expr   =
104 106
    {mutable tdesc: type_desc;
105 107
     tid: int}
......
116 118
    | Tlink of type_expr (* During unification, make links instead of substitutions *)
117 119
    | Tvar (* Monomorphic type variable *)
118 120
    | Tunivar (* Polymorphic type variable *)
121
  [@@deriving show]
119 122

  
120 123
  (*   {mutable tdesc: type_desc; *)
121 124
  (*    tid: int} *)
......
491 494
    | Tlink of type_expr (* During unification, make links instead of substitutions *)
492 495
    | Tvar (* Monomorphic type variable *)
493 496
    | Tunivar (* Polymorphic type variable *)
497
    [@@deriving show]
494 498

  
495 499
  type error =
496 500
      Unbound_value of ident  
lib/utils/utils.ml
12 12
open Graph
13 13

  
14 14
type rat = int*int
15
[@@deriving show]
15 16
type ident = string
17
[@@deriving show]
16 18
type tag = int
19
[@@deriving show]
17 20
type longident = (string * tag) list
21
[@@deriving show]
18 22

  
19 23
exception TransposeError of int*int
20 24

  
plugins/tiny/dune
1

  
2

  
3 1
(env
4 2
 (dev
5 3
  (flags
......
8 6

  
9 7
(library 
10 8
(name tiny_plugin)
11
(libraries lustrec tiny)
12
(optional)
9
(libraries yojson lustrec tiny backends)
10
(preprocess (staged_pps ppx_deriving_yojson ppx_import ppx_deriving.show))
13 11
)
plugins/tiny/tiny_results.ml
1
open Tiny
2
open Tiny_utils
3
open Yojson
4

  
5
module Make (Dom : Relational.Domain) = struct
6
  (* Take a mapping of annotations, top value of the domain and a location 
7
    and return a JSON of the form : 
8
    { "time1": "Domain description at time 1", 
9
      "time2": "Domain description at time 2"...}
10
  *)
11
  let dom_values_at_location_to_json m top l =
12
      (* Extracting associated unrolled info *)
13
      let ind = Location.MapInd.filter (fun (l',_) a -> l = l' && not(Dom.order top a)) (snd m) in
14
      let ind = Location.MapInd.bindings ind in
15
      let ind = List.sort (fun (i1, _) (i2, _) -> compare i1 i2) ind in
16
      begin
17
        `Assoc (
18
          List.map (fun ((_,i), e) ->
19
              (string_of_int i), (Dom.json e)
20
        )  ind)
21
      end
22

  
23
  let to_json mapping tiny_encoding  = 
24
    let top = Dom.top (Ast.vars_of_stm tiny_encoding.ast) in
25
    (* giving mapping of annotations and the top value of the domain first *)
26
    let dom_values_at_location_to_json = dom_values_at_location_to_json mapping top  in
27
    (* then give the location where interested in,
28
       to obtain the JSON object with the abstract value at each tick
29
    *)
30
    dom_values_at_location_to_json (Location.beg_p tiny_encoding.location_beg_while)
31
end
plugins/tiny/tiny_utils.ml
1

  
2
module Ast = Tiny.Ast
3

  
4
let gen_loc () = Tiny.Location.dummy ()
5
               
6
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Lustrec.Location.loc_start loc.Lustrec.Location.loc_end
7
                     
8
let tloc_to_lloc loc = assert false (*Lustrec.Location.dummy_loc (*TODO*) *)
9

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

  
17
let cst_bool loc b =
18
  { Ast.expr_desc =
19
      if b then
20
        Ast.Cst(Q.of_int 1, "true")
21
      else
22
        Ast.Cst(Q.of_int 0, "false");
23
    expr_loc = loc;
24
    expr_type = Ast.BoolT }
25

  
26
let cst_num loc t q =
27
{ Ast.expr_desc =
28
    Ast.Cst(q, Q.to_string q);
29
  expr_loc = loc;
30
  expr_type = t }
31
  
32
let rec real_to_q man exp =
33
  if exp = 0 then
34
        Q.of_string (Num.string_of_num man)
35
  else
36
    if exp > 0 then Q.div (real_to_q man (exp-1)) (Q.of_int 10)
37
    else (* if exp<0 then *)
38
      Q.mul
39
        (real_to_q man (exp+1))
40
        (Q.of_int 10)
41

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

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

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

  
plugins/tiny/tiny_verifier.ml
1 1
open Lustrec
2
open Backends
2 3

  
3 4
let active = ref false
4 5
let tiny_debug = ref false
6
let tiny_output = ref false
5 7
let tiny_help = ref false
6 8
let descending = ref 1
7
let unrolling = ref 0
9
let unrolling = ref 1
10
let bounds_file = ref ""
8 11

  
9 12

  
10 13
              
......
18 21
  Format.eprintf "@.@?";
19 22
  flush stdout
20 23

  
21
  
24
let generate_tiny_analysis_file basename json_tiny_analysis = 
25
  let path = !Lustrec.Options.dest_dir ^ "/" ^ basename in
26
  let destname = path ^ "_tiny.json" in 
27
  let file = open_out destname in
28
  let file_fmt = Format.formatter_of_out_channel file in
29
  Yojson.pretty_print file_fmt json_tiny_analysis;
30
  close_out file;;
31

  
22 32
let tiny_run ~basename prog machines =
23 33
  if !tiny_help then (
24 34
    let _ = print_tiny_help () in
25 35
    exit 0
26 36
  );
37
  if !bounds_file = "" then 
38
    failwith "-tiny-bounds-file <filepath> need to be set";
39
  let bound_input_file_path = !Lustrec.Options.dest_dir ^ "/" ^ !bounds_file in 
40
  let in_chan_bounds = try
41
  open_in bound_input_file_path
42
  with 
43
  | Sys_error _ -> (Format.printf "%s is not a valid path to the JSON formatted bounds constraint" bound_input_file_path; exit 2)
44
  in 
27 45
  let node_name =
28 46
    match !Lustrec.Options.main_node with
29 47
    | "" -> (
......
51 69
  let env = (* We add each variables of the node the Tiny env *)
52 70
    Tiny_utils.machine_to_env m in
53 71
  let nd = m.mname in
54
  (* Building preamble with some bounds on inputs *)
55
  (* TODO: deal woth contracts, asserts, ... *)
56
  let bounds_inputs = [] in
57
  let ast = Tiny_utils.machine_to_ast bounds_inputs m in
72
  let json_input = Yojson.Safe.from_channel in_chan_bounds in
73
  let bounds_inputs = Tiny_utils.bounds_of_yojson json_input in
74
  let bounds_inputs  = match bounds_inputs with 
75
  | Error e -> failwith e 
76
  | Ok v -> v in
77
  let tiny_encoding = Tiny_utils.machine_to_tiny_encoding bounds_inputs m in
58 78
  let mems = m.mmemory in
59 79
  
60
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
80
   Format.printf "%a@." Tiny.Ast.fprint_stm tiny_encoding.ast; 
61 81

  
62 82
   let dom =
63 83
     let open Tiny.Load_domains in
64 84
     prepare_domains (List.map get_domain !domains)
65 85
   in
66
   let results = Tiny.Analyze.analyze dom !descending !unrolling env ast in
86
   let results = Tiny.Analyze.analyze dom !descending !unrolling env tiny_encoding.ast in
67 87
   let module Results = (val results: Tiny.Analyze.Results) in
68 88
   let module Dom = Results.Dom in
69
   let module PrintResults = Tiny.PrintResults.Make (Dom) in
89
   let module JsonResults = Tiny_results.Make (Dom) in
70 90
   let m = Results.results in
71 91
   (* if !Tiny.Report.verbosity > 1 then *)
72
   PrintResults.print m ast None (* no !output_file *);
73
        (* else PrintResults.print_invariants m ast !output_file *)
92
   (* PrintResults.print m tiny_encoding.ast None (* no !output_file *); *)
93
  (* Print result analysis in JSON format on stdout *)
94
  let json_result = JsonResults.to_json m tiny_encoding in 
95
  begin 
96
    Yojson.pretty_print Format.std_formatter json_result;
97
    if !tiny_output then generate_tiny_analysis_file basename json_result;
98
  end;
99

  
74 100

  
75
   ()
76
  
77 101
  
78 102
module Verifier =
79 103
  (struct
......
97 121
        (* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain>  Print params of <domain>"); *)
98 122
        (* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
99 123
      ("-c", Arg.Set compile_mode,             " Compilation mode: compile to C");*)
100
        
124
        ("-bounds-file", Arg.Set_string bounds_file,
125
        "Path to the file containing constraints on input of the lustre code. The content of the file \
126
        must be a valid JSON containing an array of object with the following prototype : \
127
         {\"var_name\": string, \"type\": string, \"inf\": string, \"sup\": string}");
128
        "-output", Arg.Set tiny_output, "generate a __tiny_analysis.json";
101 129
        ("-quiet", Arg.Unit quiet, " Quiet mode");
102 130
        (* ("-q", Arg.Unit quiet, " Quiet mode"); *)
103 131
        ("-verbose", Arg.Set_int Tiny.Report.verbosity,
......
109 137
        ("-o", Arg.String set_output_file,
110 138
         "<filename>  Output results to file <filename> (default is standard ouput)");
111 139
   *)
112
        ("-descending", Arg.Set_int descending,
140
      (*  ("-descending", Arg.Set_int descending,
113 141
         "<n>  Perform <n> descending iterations after fixpoint of a loop \
114
          is reached (default is 1)");
142
          is reached (default is 1)");*)
115 143
        (* ("-d", Arg.Set_int descending,
116 144
         *  "<n>  Perform <n> descending iterations after fixpoint of a loop \
117 145
         * is reached (default is 1)"); *)
118
      ("-unrolling", Arg.Set_int unrolling,
119
       "<n>  Unroll loops <n> times before computing fixpoint (default is 0)");
146
      ("-duration", Arg.Set_int unrolling,
147
       "<n>  Duration, the number of steps of the simulation");
120 148
      (* (\* ("-u", Arg.Set_int unrolling,
121 149
       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
122 150
       "-help", Arg.Set tiny_help, "tiny help and usage";
......
126 154
      
127 155
    let activate () =
128 156
      active := true;
129
      (* Lustrec.Options.global_inline := true;
130
       * Lustrec.Options.optimization := 0;
131
       * Lustrec.Options.const_unfold := true; *)
157
      Lustrec.Options.output := "tiny";
158
      Lustrec.Options.global_inline := true;
159
      Lustrec.Options.optimization := 0;
160
      Lustrec.Options.const_unfold := true;
132 161
      ()
133 162
      
134 163
    let is_active () = !active
src/compiler_stages.ml
3 3
open Lustrec.Utils
4 4
open Compiler_common
5 5
open Lustrec.Lustre_types
6
open Backends
7

  
6 8
module Mpfr = Lustrec_mpfr
7 9

  
8 10
exception StopPhase1 of program_t
......
293 295
      begin
294 296
      	Lustrec.Log.report ~level:1 (fun fmt -> fprintf fmt ".. no C code generation for lusi@,");
295 297
      end
298
  | "tiny", ".lus" -> 
299
  begin
300
    Tiny_backend.translate_to_tiny basename prog machine_code dependencies
301
  end
296 302
  | "java", _ ->
297 303
     begin
298 304
       (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)

Also available in: Unified diff