Project

General

Profile

Download (12.3 KB) Statistics
| Branch: | Tag: | Revision:
1 ca7ff3f7 Lélio Brun
open Lustre_types
2 40d33d55 xavier.thirioux
open Corelang
3
open Log
4
5 ca7ff3f7 Lélio Brun
module IdSet = Set.Make (struct
6
  type t = expr * int
7 40d33d55 xavier.thirioux
8 ca7ff3f7 Lélio Brun
  let compare = compare
9
end)
10
11
let inout_vars = ref []
12 40d33d55 xavier.thirioux
13 3e1d20e0 ploc
(* This was used to add inout variables in the final signature. May have to be
14
   reactivated later *)
15 ca7ff3f7 Lélio Brun
16 3e1d20e0 ploc
(* let print_tautology_var fmt v = *)
17
(*   match (Types.repr v.var_type).Types.tdesc with *)
18
(*   | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)
19 ca7ff3f7 Lélio Brun
(* | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
20
(* | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
21
(* | _ -> Format.fprintf fmt "(true)" *)
22 40d33d55 xavier.thirioux
23 3e1d20e0 ploc
(* let print_path arg = match !inout_vars with *)
24
(*   | [] -> Format.printf "%t@." arg   *)
25 ca7ff3f7 Lélio Brun
(* | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun
26
   fmt elem -> print_tautology_var fmt elem)) l *)
27 40d33d55 xavier.thirioux
28 ca7ff3f7 Lélio Brun
let rel_op = [ "="; "!="; "<"; "<="; ">"; ">=" ]
29 40d33d55 xavier.thirioux
30 3e1d20e0 ploc
(* Used when we were printing the expression directly. Now we are constructing
31
   them as regular expressions.
32
33
   let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf
34 ca7ff3f7 Lélio Brun
   fmt "pre "; print_pre fmt (nb_pre-1) ) *)
35 40d33d55 xavier.thirioux
36 ca7ff3f7 Lélio Brun
let mk_pre n e = if n <= 0 then e else mkexpr e.expr_loc (Expr_pre e)
37 40d33d55 xavier.thirioux
38 ca7ff3f7 Lélio Brun
(* let combine2 f sub1 sub2 = let elem_e1 = List.fold_right IdSet.add (List.map
39
   fst sub1) IdSet.empty in let elem_e2 = List.fold_right IdSet.add (List.map
40
   fst sub2) IdSet.empty in let common = IdSet.inter elem_e1 elem_e2 in let
41
   sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
42
   let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2
43
   in (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @ (List.map
44
   (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @ (List.map (fun v -> (v,
45
   {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)})
46
   (IdSet.elements common)) ) *)
47 3e1d20e0 ploc
48 ca7ff3f7 Lélio Brun
let rec select (v : expr * int) (active : bool list)
49
    (modified : ((expr * int) * expr) list list) (orig : expr list) =
50
  match active, modified, orig with
51
  | true :: active_tl, e :: modified_tl, _ :: orig_tl ->
52
    List.assoc v e :: select v active_tl modified_tl orig_tl
53
  | false :: active_tl, _ :: modified_tl, e :: orig_tl ->
54
    e :: select v active_tl modified_tl orig_tl
55
  | [], [], [] ->
56
    []
57
  | _ ->
58
    assert false
59 2104c80a ploc
60 ca7ff3f7 Lélio Brun
let combine (f : expr list -> expr) subs orig : ((expr * int) * expr) list =
61
  let elems =
62
    List.map
63
      (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty)
64
      subs
65
  in
66
  let all = List.fold_right IdSet.union elems IdSet.empty in
67
  List.map
68
    (fun v ->
69
      let active_subs = List.map (IdSet.mem v) elems in
70
      v, f (select v active_subs subs orig))
71
    (IdSet.elements all)
72
73
(* In a previous version, the printer was introducing fake description, ie
74
   tautologies, over inout variables to make sure they were not suppresed by
75
   some other algorithms *)
76
77
(* Takes the variable on which these coverage criteria will apply, as well as
78
   the expression and its negated version. Returns the expr and the variable
79
   expression, as well as the two new boolean expressions descibing the two
80
   associated modes. *)
81 2104c80a ploc
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =
82 3e1d20e0 ploc
  let loc = expr.expr_loc in
83 ca7ff3f7 Lélio Brun
  let not_vi_as_expr = mkpredef_call loc "not" [ vi_as_expr ] in
84 2104c80a ploc
  let expr1, expr2 =
85 ca7ff3f7 Lélio Brun
    if nb_elems > 1 then
86
      let changed_expr = mkpredef_call loc "!=" [ expr; expr_neg_vi ] in
87
      let expr1 = mkpredef_call loc "&&" [ vi_as_expr; changed_expr ] in
88
      let expr2 = mkpredef_call loc "&&" [ not_vi_as_expr; changed_expr ] in
89 2104c80a ploc
      expr1, expr2
90 ca7ff3f7 Lélio Brun
    else vi_as_expr, not_vi_as_expr
91 2104c80a ploc
  in
92 ca7ff3f7 Lélio Brun
  (expr, vi_as_expr), [ true, expr1; false, expr2 ]
93
(* expr1 corresponds to atom true while expr2 corresponds to atom false *)
94
95
(* Format.printf "%a@." Printers.pp_expr expr1;  *)
96
(* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
97
(*   Printers.pp_expr vi_as_expr *)
98
(*   Printers.pp_expr expr (\*v*\) *)
99
(*   Printers.pp_expr expr_neg_vi); *)
100
(* Format.printf "%a@." Printers.pp_expr expr2;  *)
101
(* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
102
(*   Printers.pp_expr vi_as_expr *)
103
(*   Printers.pp_expr expr (\*v*\) *)
104
(*   Printers.pp_expr expr_neg_vi) *)
105 3e1d20e0 ploc
106 ca7ff3f7 Lélio Brun
let rec compute_neg_expr cpt_pre (expr : Lustre_types.expr) =
107
  let neg_list l =
108
    List.fold_right
109
      (fun e (vl, el) ->
110
        let vl', e' = compute_neg_expr cpt_pre e in
111
        vl' @ vl, e' :: el)
112
      l ([], [])
113 3e1d20e0 ploc
  in
114 40d33d55 xavier.thirioux
  match expr.expr_desc with
115 ca7ff3f7 Lélio Brun
  | Expr_tuple l ->
116
    let vl, neg = neg_list l in
117
    vl, combine (fun l' -> { expr with expr_desc = Expr_tuple l' }) neg l
118
  | Expr_ite (i, t, e) when Types.is_bool_type t.expr_type ->
119
    let list = [ i; t; e ] in
120 3e1d20e0 ploc
    let vl, neg = neg_list list in
121 ca7ff3f7 Lélio Brun
    ( vl,
122
      combine
123
        (fun l ->
124
          match l with
125
          | [ i'; t'; e' ] ->
126
            { expr with expr_desc = Expr_ite (i', t', e') }
127
          | _ ->
128
            assert false)
129
        neg list )
130
  | Expr_ite (i, t, e) ->
131
    (* We return the guard as a new guard *)
132 3e1d20e0 ploc
    let vl = gen_mcdc_cond_guard i in
133 ca7ff3f7 Lélio Brun
    let list = [ i; t; e ] in
134 3e1d20e0 ploc
    let vl', neg = neg_list list in
135 ca7ff3f7 Lélio Brun
    ( vl @ vl',
136
      combine
137
        (fun l ->
138
          match l with
139
          | [ i'; t'; e' ] ->
140
            { expr with expr_desc = Expr_ite (i', t', e') }
141
          | _ ->
142
            assert false)
143
        neg list )
144
  | Expr_arrow (e1, e2) ->
145
    let vl1, e1' = compute_neg_expr cpt_pre e1 in
146
    let vl2, e2' = compute_neg_expr cpt_pre e2 in
147
    ( vl1 @ vl2,
148
      combine
149
        (fun l ->
150
          match l with
151
          | [ x; y ] ->
152
            { expr with expr_desc = Expr_arrow (x, y) }
153
          | _ ->
154
            assert false)
155
        [ e1'; e2' ] [ e1; e2 ] )
156 3e1d20e0 ploc
  | Expr_pre e ->
157 ca7ff3f7 Lélio Brun
    let vl, e' = compute_neg_expr (cpt_pre + 1) e in
158
    ( vl,
159
      List.map (fun (v, negv) -> v, { expr with expr_desc = Expr_pre negv }) e'
160
    )
161 ca7e8027 Lélio Brun
  | Expr_appl (op_name, _, _) when List.mem op_name rel_op ->
162 ca7ff3f7 Lélio Brun
    [], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
163 3e1d20e0 ploc
  | Expr_appl (op_name, args, r) ->
164 ca7ff3f7 Lélio Brun
    let vl, args' = compute_neg_expr cpt_pre args in
165
    ( vl,
166
      List.map
167
        (fun (v, negv) ->
168
          v, { expr with expr_desc = Expr_appl (op_name, negv, r) })
169
        args' )
170
  | Expr_ident _ when Types.is_bool_type expr.expr_type ->
171
    [], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
172
  | _ ->
173
    [] (* empty vars *), []
174 40d33d55 xavier.thirioux
175 3e1d20e0 ploc
and gen_mcdc_cond_var v expr =
176
  report ~level:1 (fun fmt ->
177 ca7ff3f7 Lélio Brun
      Format.fprintf fmt
178
        ".. Generating MC/DC cond for boolean flow %s and expression %a@." v
179 2104c80a ploc
        Printers.pp_expr expr);
180 3e1d20e0 ploc
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
181 ca7ff3f7 Lélio Brun
  let len = List.length leafs_n_neg_expr in
182
  if len >= 1 then
183
    List.fold_left
184
      (fun accu ((vi, nb_pre), expr_neg_vi) ->
185
        mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi :: accu)
186
      vl leafs_n_neg_expr
187
  else vl
188 40d33d55 xavier.thirioux
189
and gen_mcdc_cond_guard expr =
190 3e1d20e0 ploc
  report ~level:1 (fun fmt ->
191 ca7ff3f7 Lélio Brun
      Format.fprintf fmt ".. Generating MC/DC cond for guard %a@."
192 2104c80a ploc
        Printers.pp_expr expr);
193 3e1d20e0 ploc
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
194 2104c80a ploc
  let len = List.length leafs_n_neg_expr in
195 ca7ff3f7 Lélio Brun
  if len >= 1 then
196
    List.fold_left
197
      (fun accu ((vi, nb_pre), expr_neg_vi) ->
198
        mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi :: accu)
199
      vl leafs_n_neg_expr
200
  else vl
201 40d33d55 xavier.thirioux
202 ca7ff3f7 Lélio Brun
let rec mcdc_expr cpt_pre expr =
203 40d33d55 xavier.thirioux
  match expr.expr_desc with
204 3e1d20e0 ploc
  | Expr_tuple l ->
205 ca7ff3f7 Lélio Brun
    let vl =
206
      List.fold_right
207
        (fun e accu_v ->
208
          let vl = mcdc_expr cpt_pre e in
209
          vl @ accu_v)
210
        l []
211
    in
212
    vl
213
  | Expr_ite (i, t, e) ->
214
    let vl_i = gen_mcdc_cond_guard i in
215
    let vl_t = mcdc_expr cpt_pre t in
216
    let vl_e = mcdc_expr cpt_pre e in
217
    vl_i @ vl_t @ vl_e
218 3e1d20e0 ploc
  | Expr_arrow (e1, e2) ->
219 ca7ff3f7 Lélio Brun
    let vl1 = mcdc_expr cpt_pre e1 in
220
    let vl2 = mcdc_expr cpt_pre e2 in
221
    vl1 @ vl2
222 3e1d20e0 ploc
  | Expr_pre e ->
223 ca7ff3f7 Lélio Brun
    let vl = mcdc_expr (cpt_pre + 1) e in
224
    vl
225 ca7e8027 Lélio Brun
  | Expr_appl (_, args, _) ->
226 ca7ff3f7 Lélio Brun
    let vl = mcdc_expr cpt_pre args in
227
    vl
228
  | _ ->
229
    []
230 40d33d55 xavier.thirioux
231 ca7ff3f7 Lélio Brun
let mcdc_var_def v expr =
232 66359a5e ploc
  if Types.is_bool_type expr.expr_type then
233 ca7ff3f7 Lélio Brun
    let vl = gen_mcdc_cond_var v expr in
234
    vl
235 66359a5e ploc
  else
236
    let vl = mcdc_expr 0 expr in
237
    vl
238 ca7ff3f7 Lélio Brun
239 40d33d55 xavier.thirioux
let mcdc_node_eq eq =
240 3e1d20e0 ploc
  let vl =
241 ca7ff3f7 Lélio Brun
    match
242
      ( eq.eq_lhs,
243
        Types.is_bool_type eq.eq_rhs.expr_type,
244
        (Types.repr eq.eq_rhs.expr_type).Types.tdesc,
245
        eq.eq_rhs.expr_desc )
246
    with
247
    | [ lhs ], true, _, _ ->
248
      gen_mcdc_cond_var lhs eq.eq_rhs
249
    | _ :: _, false, Types.Ttuple _, Expr_tuple rhs ->
250
      (* We iterate trough pairs, but accumulate variables aside. The resulting
251
         expression shall remain a tuple defintion *)
252
      let vl =
253
        List.fold_right2
254
          (fun lhs rhs accu ->
255
            let v = mcdc_var_def lhs rhs in
256
            (* we don't care about the expression it. We focus on the coverage
257
               expressions in v *)
258
            v @ accu)
259
          eq.eq_lhs rhs []
260
      in
261
      vl
262
    | _ ->
263
      mcdc_expr 0 eq.eq_rhs
264 3e1d20e0 ploc
  in
265
  vl
266 40d33d55 xavier.thirioux
267 bde99c3f xavier.thirioux
let mcdc_node_stmt stmt =
268
  match stmt with
269 ca7ff3f7 Lélio Brun
  | Eq eq ->
270
    let vl = mcdc_node_eq eq in
271
    vl
272
  | Aut _ ->
273
    assert false
274 bde99c3f xavier.thirioux
275 ca7ff3f7 Lélio Brun
let mcdc_top_decl td =
276 40d33d55 xavier.thirioux
  match td.top_decl_desc with
277 3e1d20e0 ploc
  | Node nd ->
278 ca7ff3f7 Lélio Brun
    let new_coverage_exprs =
279
      List.fold_right
280
        (fun s accu_v ->
281
          let vl' = mcdc_node_stmt s in
282
          vl' @ accu_v)
283
        nd.node_stmts []
284
    in
285
    (* We add coverage vars as boolean internal flows. *)
286
    let fresh_cov_defs =
287
      List.flatten
288
        (List.map
289
           (fun ((_, atom), expr_l) ->
290
             List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l)
291
           new_coverage_exprs)
292
    in
293
    let nb_total = List.length fresh_cov_defs in
294
    let fresh_cov_vars =
295
      List.mapi
296
        (fun i (atom, atom_valid, cov_expr) ->
297
          let loc = cov_expr.expr_loc in
298
          Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
299
          let cov_id = Format.flush_str_formatter () in
300
          let cov_var =
301
            mkvar_decl loc
302
              ( cov_id,
303
                mktyp loc Tydec_bool,
304
                mkclock loc Ckdec_any,
305
                false,
306
                None,
307
                None )
308
          in
309
          let cov_def = Eq (mkeq loc ([ cov_id ], cov_expr)) in
310
          cov_var, cov_def, atom, atom_valid)
311
        fresh_cov_defs
312
    in
313
    let fresh_vars, fresh_eqs =
314
      List.fold_right
315
        (fun (v, eq, _, _) (accuv, accueq) -> v :: accuv, eq :: accueq)
316
        fresh_cov_vars ([], [])
317
    in
318
    let fresh_annots =
319
      (* We produce two sets of annotations: PROPERTY ones for kind2, and
320
         regular ones to keep track of the nature of the annotations. *)
321
      List.map
322
        (fun (v, _, atom, atom_valid) ->
323
          let e = expr_of_vdecl v in
324
          let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [ e ]) in
325
          {
326
            annots =
327
              [
328
                [ "PROPERTY" ], neg_ee;
329
                (* Using negated property to force model-checker to produce a
330
                   suitable covering trace *)
331
                (let loc = Location.dummy_loc in
332
                 let valid_e =
333
                   let open Corelang in
334
                   mkexpr loc (Expr_const (const_of_bool atom_valid))
335
                 in
336
                 ( [ "coverage"; "mcdc"; v.var_id ],
337
                   expr_to_eexpr
338
                     (Corelang.expr_of_expr_list loc [ e; atom; valid_e ]) ));
339
              ];
340
            annot_loc = v.var_loc;
341
          })
342
        fresh_cov_vars
343
    in
344
    Format.printf "%i coverage criteria generated for node %s@ " nb_total
345
      nd.node_id;
346
    (* And add them as annotations --%PROPERTY: var TODO *)
347
    {
348
      td with
349
      top_decl_desc =
350
        Node
351
          {
352
            nd with
353
            node_locals = nd.node_locals @ fresh_vars;
354
            node_stmts = nd.node_stmts @ fresh_eqs;
355
            node_annot = nd.node_annot @ fresh_annots;
356
          };
357
    }
358
  | _ ->
359
    td
360 40d33d55 xavier.thirioux
361
let mcdc prog =
362 ca7ff3f7 Lélio Brun
  (* If main node is provided add silly constraints to show in/out variables in
363
     the path condition *)
364
  (if !Options.main_node <> "" then
365
   inout_vars :=
366
     let top =
367
       List.find
368
         (fun td ->
369
           match td.top_decl_desc with
370
           | Node nd when nd.node_id = !Options.main_node ->
371
             true
372
           | _ ->
373
             false)
374
         prog
375
     in
376
     match top.top_decl_desc with
377
     | Node nd ->
378
       nd.node_inputs @ nd.node_outputs
379
     | _ ->
380
       assert false);
381 3e1d20e0 ploc
  List.map mcdc_top_decl prog
382 40d33d55 xavier.thirioux
383
(* Local Variables: *)
384
(* compile-command:"make -C .." *)
385
(* End: *)