Project

General

Profile

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

    
5
module IdSet = Set.Make (struct type t = expr * int let compare = compare end)
6

    
7
let inout_vars = ref [] 
8

    
9
(* This was used to add inout variables in the final signature. May have to be
10
   reactivated later *)
11
  
12
(* let print_tautology_var fmt v = *)
13
(*   match (Types.repr v.var_type).Types.tdesc with *)
14
(*   | Types.Tbool -> Format.fprintf fmt "(%s or not %s)" v.var_id v.var_id *)
15
(*   | Types.Tint -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
16
(*   | Types.Treal -> Format.fprintf fmt "(%s > 0 or %s <= 0)" v.var_id v.var_id *)
17
(*   | _ -> Format.fprintf fmt "(true)" *)
18

    
19
(* let print_path arg = match !inout_vars with *)
20
(*   | [] -> Format.printf "%t@." arg   *)
21
(*   | l -> Format.printf "%t and %a@." arg (Utils.fprintf_list ~sep:" and " (fun fmt elem -> print_tautology_var fmt elem)) l *)
22

    
23
let rel_op = ["="; "!="; "<"; "<="; ">" ; ">=" ]
24

    
25
(* Used when we were printing the expression directly. Now we are constructing
26
   them as regular expressions.
27

    
28
   let rec print_pre fmt nb_pre = if nb_pre <= 0 then () else ( Format.fprintf
29
   fmt "pre "; print_pre fmt (nb_pre-1) )
30
*)
31
  
32
let mk_pre n e =
33
  if n <= 0 then
34
    e
35
  else
36
    mkexpr e.expr_loc (Expr_pre e)
37
   
38
(*
39
   let combine2 f sub1 sub2 = 
40
   let elem_e1 = List.fold_right IdSet.add (List.map fst sub1) IdSet.empty in
41
   let elem_e2 = List.fold_right IdSet.add (List.map fst sub2) IdSet.empty in
42
   let common = IdSet.inter elem_e1 elem_e2 in
43
   let sub1_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub1 in
44
   let sub2_filtered = List.filter (fun (v, _) -> not (IdSet.mem v common)) sub2 in
45
   (List.map (fun (v, negv) -> (v, f negv e2)) sub1_filtered) @
46
   (List.map (fun (v, negv) -> (v, f e1 negv)) sub2_filtered) @
47
   (List.map (fun v -> (v, {expr with expr_desc = Expr_arrow(List.assoc v sub1, List.assoc v sub2)}) (IdSet.elements common))      )
48
*)
49

    
50
let rec select (v: expr * int) (active: bool list) (modified: ((expr * int) * expr) list list) (orig: expr list) =
51
match active, modified, orig with
52
| true::active_tl, e::modified_tl, _::orig_tl -> (List.assoc v e)::(select v active_tl modified_tl orig_tl)
53
| false::active_tl, _::modified_tl, e::orig_tl -> e::(select v active_tl modified_tl orig_tl)
54
| [], [], [] -> []
55
| _ -> assert false
56
  
57
let combine (f: expr list -> expr ) subs orig : ((expr * int) * expr) list  = 
58
  let elems = List.map (fun sub_i -> List.fold_right IdSet.add (List.map fst sub_i) IdSet.empty) subs in
59
  let all = List.fold_right IdSet.union elems IdSet.empty in
60
  List.map (fun v ->
61
    let active_subs = List.map (IdSet.mem v) elems in
62
    v, f (select v active_subs subs orig)
63
  ) (IdSet.elements all)
64

    
65

    
66
(* In a previous version, the printer was introducing fake
67
   description, ie tautologies, over inout variables to make sure they
68
   were not suppresed by some other algorithms *)
69

    
70
(* Takes the variable on which these coverage criteria will apply, as
71
   well as the expression and its negated version. Returns the expr
72
   and the variable expression, as well as the two new boolean
73
   expressions descibing the two associated modes. *)
74
let mcdc_var vi_as_expr nb_elems expr expr_neg_vi =
75
  let loc = expr.expr_loc in
76
  let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in
77
  let expr1, expr2 =
78
    if nb_elems > 1 then 
79
      let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in
80
      let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in
81
      let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in
82
      expr1, expr2
83
    else
84
      vi_as_expr, not_vi_as_expr
85
  in
86
  ((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom
87
                                                     true while expr2
88
                                                     corresponds to atom
89
                                                     false *)
90

    
91
  (* Format.printf "%a@." Printers.pp_expr expr1;  *)
92
  (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
93
  (*   Printers.pp_expr vi_as_expr *)
94
  (*   Printers.pp_expr expr (\*v*\) *)
95
  (*   Printers.pp_expr expr_neg_vi); *)
96
  (* Format.printf "%a@." Printers.pp_expr expr2;  *)
97
  (* print_path (fun fmt -> Format.fprintf fmt "(not %a) and (%a != %a)" *)
98
  (*   Printers.pp_expr vi_as_expr *)
99
  (*   Printers.pp_expr expr (\*v*\) *)
100
  (*   Printers.pp_expr expr_neg_vi) *)
101
    
102
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =
103
  let neg_list l = 
104
    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
105
  in
106
  match expr.expr_desc with
107
  | Expr_tuple l -> 
108
     let vl, neg = neg_list l in
109
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
110
     
111
  | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> (
112
    let list = [i; t; e] in
113
    let vl, neg = neg_list list in
114
    vl, combine (fun l ->
115
            match l with
116
            | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
117
            | _ -> assert false
118
          ) neg list
119
  )
120
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
121
    let vl = gen_mcdc_cond_guard i in
122
    let list = [i; t; e] in
123
    let vl', neg = neg_list list in
124
    vl@vl', combine (fun l ->
125
                match l with
126
                | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
127
                | _ -> assert false
128
              ) neg list
129
  )
130
  | Expr_arrow (e1, e2) -> 
131
     let vl1, e1' = compute_neg_expr cpt_pre e1 in
132
     let vl2, e2' = compute_neg_expr cpt_pre e2 in
133
     vl1@vl2, combine (fun l -> match l with
134
                                | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
135
                                | _ -> assert false
136
                ) [e1'; e2'] [e1; e2]
137

    
138
  | Expr_pre e ->
139
     let vl, e' = compute_neg_expr (cpt_pre+1) e in
140
     vl, List.map
141
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
142

    
143
  | Expr_appl (op_name, _, _) when List.mem op_name rel_op ->
144
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
145

    
146
  | Expr_appl (op_name, args, r) ->
147
     let vl, args' = compute_neg_expr cpt_pre args in
148
     vl, List.map 
149
           (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
150
           args'
151

    
152
  | Expr_ident _ when (Types.is_bool_type expr.expr_type) ->
153
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
154
  | _ -> [] (* empty vars *) , [] 
155
and gen_mcdc_cond_var v expr =
156
  report ~level:1 (fun fmt ->
157
      Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
158
        v
159
        Printers.pp_expr expr);
160
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
161
  let len = List.length leafs_n_neg_expr in 
162
  if len >= 1 then (
163
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
164
        (mcdc_var  (mk_pre nb_pre vi) len expr expr_neg_vi)::accu
165
      ) vl leafs_n_neg_expr
166
  )
167
  else
168
    vl
169

    
170
and gen_mcdc_cond_guard expr =
171
  report ~level:1 (fun fmt ->
172
      Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
173
        Printers.pp_expr expr);
174
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
175
  let len = List.length leafs_n_neg_expr in
176
  if len >= 1 then (
177
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
178
        (mcdc_var (mk_pre nb_pre vi) len expr expr_neg_vi)::accu
179
      ) vl leafs_n_neg_expr)
180
  else
181
    vl
182
  
183

    
184
let rec mcdc_expr cpt_pre expr = 
185
  match expr.expr_desc with
186
  | Expr_tuple l ->
187
     let vl =
188
       List.fold_right (fun e accu_v ->
189
	 let vl = mcdc_expr cpt_pre e in
190
	 (vl@accu_v))
191
	 l
192
	 []
193
     in
194
     vl
195
  | Expr_ite (i,t,e) ->
196
     let vl_i = gen_mcdc_cond_guard i in
197
     let vl_t = mcdc_expr cpt_pre t in
198
     let vl_e = mcdc_expr cpt_pre e in
199
     vl_i@vl_t@vl_e
200
  | Expr_arrow (e1, e2) ->
201
     let vl1 = mcdc_expr cpt_pre e1 in
202
     let vl2 = mcdc_expr cpt_pre e2 in
203
     vl1@vl2
204
  | Expr_pre e ->
205
     let vl = mcdc_expr (cpt_pre+1) e in
206
     vl
207
  | Expr_appl (_, args, _) ->
208
     let vl = mcdc_expr cpt_pre args in
209
     vl
210
  | _ -> []
211

    
212
let mcdc_var_def v expr = 
213
  if Types.is_bool_type expr.expr_type then
214
     let vl = gen_mcdc_cond_var v expr in
215
     vl
216
  else
217
    let vl = mcdc_expr 0 expr in
218
    vl
219
      
220
let mcdc_node_eq eq =
221
  let vl =
222
    match eq.eq_lhs, Types.is_bool_type eq.eq_rhs.expr_type, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
223
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
224
    | _::_, false, Types.Ttuple _, Expr_tuple rhs ->
225
       (* We iterate trough pairs, but accumulate variables aside. The resulting
226
	  expression shall remain a tuple defintion *)
227
       let vl = List.fold_right2 (fun lhs rhs accu ->
228
	 let v = mcdc_var_def lhs rhs in
229
	 (* we don't care about the expression it. We focus on the coverage
230
	    expressions in v *)
231
	 v@accu
232
       ) eq.eq_lhs rhs []
233
       in
234
       vl
235
    | _ -> mcdc_expr 0 eq.eq_rhs 
236
  in
237
  vl
238

    
239
let mcdc_node_stmt stmt =
240
  match stmt with
241
  | Eq eq -> let vl = mcdc_node_eq eq in vl
242
  | Aut _ -> assert false
243

    
244
let mcdc_top_decl td = 
245
  match td.top_decl_desc with
246
  | Node nd ->
247
     let new_coverage_exprs =
248
       List.fold_right (
249
	   fun s accu_v ->
250
	   let vl' = mcdc_node_stmt s in
251
	   vl'@accu_v
252
	 ) nd.node_stmts []
253
     in
254
     (* We add coverage vars as boolean internal flows. *)
255
     let fresh_cov_defs = List.flatten (List.map (fun ((_, atom), expr_l) -> List.map (fun (atom_valid, case) -> atom, atom_valid, case) expr_l) new_coverage_exprs) in
256
     let nb_total = List.length fresh_cov_defs in
257
     let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) ->
258
				     let loc = cov_expr.expr_loc in
259
				     Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
260
				     let cov_id = Format.flush_str_formatter () in
261
				     let cov_var = mkvar_decl loc
262
							      (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in
263
				     let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
264
				     cov_var, cov_def, atom, atom_valid
265
				    ) fresh_cov_defs
266
     in
267
     let fresh_vars, fresh_eqs =
268
       List.fold_right
269
	 (fun (v,eq,_,_) (accuv, accueq)-> v::accuv, eq::accueq )
270
	 fresh_cov_vars
271
	 ([], [])
272
     in
273
     let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for
274
			   kind2, and regular ones to keep track of the nature
275
			   of the annotations. *)
276
       List.map
277
	 (fun (v, _, atom, atom_valid) ->
278
	  let e = expr_of_vdecl v in
279
	  let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in
280
	  {annots =  [["PROPERTY"], neg_ee; (* Using negated property to force
281
                                               model-checker to produce a
282
                                               suitable covering trace *)
283
                      let loc = Location.dummy_loc in
284
		      let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in
285
		      ["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e])
286
		     ];
287
	   annot_loc = v.var_loc})
288
	 fresh_cov_vars
289
     in
290
     Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;
291
     (* And add them as annotations --%PROPERTY: var TODO *)
292
     {td with top_decl_desc = Node {nd with
293
				     node_locals = nd.node_locals@fresh_vars;
294
				     node_stmts = nd.node_stmts@fresh_eqs;
295
				     node_annot = nd.node_annot@fresh_annots
296
				   }}
297
  | _ -> td
298

    
299

    
300
let mcdc prog =
301
  (* If main node is provided add silly constraints to show in/out variables in the path condition *)
302
  if !Options.main_node <> "" then (
303
    inout_vars := 
304
      let top = List.find 
305
	(fun td -> 
306
	  match td.top_decl_desc with 
307
	  | Node nd when nd.node_id = !Options.main_node -> true
308
	  | _ -> false) 
309
	prog 
310
      in
311
      match top.top_decl_desc with
312
      | Node nd -> nd.node_inputs @ nd.node_outputs
313
      | _ -> assert false);
314
  List.map mcdc_top_decl prog
315

    
316

    
317
    
318
(* Local Variables: *)
319
(* compile-command:"make -C .." *)
320
(* End: *)
321

    
322
    
(49-49/66)