Project

General

Profile

Download (12.3 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustre_types
2
open Corelang
3
open Log
4

    
5
module IdSet = Set.Make (struct
6
  type t = expr * int
7

    
8
  let compare = compare
9
end)
10

    
11
let inout_vars = ref []
12

    
13
(* This was used to add inout variables in the final signature. May have to be
14
   reactivated later *)
15

    
16
(* 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
(* | 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

    
23
(* let print_path arg = match !inout_vars with *)
24
(*   | [] -> Format.printf "%t@." arg   *)
25
(* | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun
26
   fmt elem -> print_tautology_var fmt elem)) l *)
27

    
28
let rel_op = [ "="; "!="; "<"; "<="; ">"; ">=" ]
29

    
30
(* 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
   fmt "pre "; print_pre fmt (nb_pre-1) ) *)
35

    
36
let mk_pre n e = if n <= 0 then e else mkexpr e.expr_loc (Expr_pre e)
37

    
38
(* 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

    
48
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

    
60
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
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =
82
  let loc = expr.expr_loc in
83
  let not_vi_as_expr = mkpredef_call loc "not" [ vi_as_expr ] in
84
  let expr1, expr2 =
85
    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
      expr1, expr2
90
    else vi_as_expr, not_vi_as_expr
91
  in
92
  (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

    
106
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
  in
114
  match expr.expr_desc with
115
  | 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
    let vl, neg = neg_list list in
121
    ( 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
    let vl = gen_mcdc_cond_guard i in
133
    let list = [ i; t; e ] in
134
    let vl', neg = neg_list list in
135
    ( 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
  | Expr_pre e ->
157
    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
  | Expr_appl (op_name, _, _) when List.mem op_name rel_op ->
162
    [], [ (expr, cpt_pre), mkpredef_call expr.expr_loc "not" [ expr ] ]
163
  | Expr_appl (op_name, args, r) ->
164
    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

    
175
and gen_mcdc_cond_var v expr =
176
  report ~level:1 (fun fmt ->
177
      Format.fprintf fmt
178
        ".. Generating MC/DC cond for boolean flow %s and expression %a@." v
179
        Printers.pp_expr expr);
180
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
181
  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

    
189
and gen_mcdc_cond_guard expr =
190
  report ~level:1 (fun fmt ->
191
      Format.fprintf fmt ".. Generating MC/DC cond for guard %a@."
192
        Printers.pp_expr expr);
193
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
194
  let len = List.length leafs_n_neg_expr in
195
  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

    
202
let rec mcdc_expr cpt_pre expr =
203
  match expr.expr_desc with
204
  | Expr_tuple l ->
205
    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
  | Expr_arrow (e1, e2) ->
219
    let vl1 = mcdc_expr cpt_pre e1 in
220
    let vl2 = mcdc_expr cpt_pre e2 in
221
    vl1 @ vl2
222
  | Expr_pre e ->
223
    let vl = mcdc_expr (cpt_pre + 1) e in
224
    vl
225
  | Expr_appl (_, args, _) ->
226
    let vl = mcdc_expr cpt_pre args in
227
    vl
228
  | _ ->
229
    []
230

    
231
let mcdc_var_def v expr =
232
  if Types.is_bool_type expr.expr_type then
233
    let vl = gen_mcdc_cond_var v expr in
234
    vl
235
  else
236
    let vl = mcdc_expr 0 expr in
237
    vl
238

    
239
let mcdc_node_eq eq =
240
  let vl =
241
    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
  in
265
  vl
266

    
267
let mcdc_node_stmt stmt =
268
  match stmt with
269
  | Eq eq ->
270
    let vl = mcdc_node_eq eq in
271
    vl
272
  | Aut _ ->
273
    assert false
274

    
275
let mcdc_top_decl td =
276
  match td.top_decl_desc with
277
  | Node nd ->
278
    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

    
361
let mcdc prog =
362
  (* 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
  List.map mcdc_top_decl prog
382

    
383
(* Local Variables: *)
384
(* compile-command:"make -C .." *)
385
(* End: *)
(49-49/66)