Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ e6b644f4

History | View | Annotate | Download (11.7 KB)

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