Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ e8250987

History | View | Annotate | Download (11.5 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
(* In a previous version, the printer was introducing fake description, ie
68
   tautologies, over inout variables to make sure they were not suppresed by
69
   some other algorithms *)
70
71
(* Takes the variable on which these coverage criteria will apply, as well as
72
   the expression and its negated version. Returns the expr and the variable
73
   expression, as well as the two new boolean expressions descibing the two
74
   associated modes. *)
75
let mcdc_var vi_as_expr expr expr_neg_vi =
76
  let loc = expr.expr_loc in
77
  let changed_expr = mkpredef_call loc "!=" [expr; expr_neg_vi] in
78
  let not_vi_as_expr = mkpredef_call loc "not" [vi_as_expr] in
79
  let expr1 = mkpredef_call loc "&&" [vi_as_expr; changed_expr] in
80
  let expr2 = mkpredef_call loc "&&" [not_vi_as_expr; changed_expr] in
81 8cacf677 ploc
  ((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom
82
                                                     true while expr2
83
                                                     corresponds to atom
84
                                                     false *)
85 3e1d20e0 ploc
86
  (* Format.printf "%a@." Printers.pp_expr expr1;  *)
87
  (* print_path (fun fmt -> Format.fprintf fmt "%a and (%a != %a)" *)
88
  (*   Printers.pp_expr vi_as_expr *)
89
  (*   Printers.pp_expr expr (\*v*\) *)
90
  (*   Printers.pp_expr expr_neg_vi); *)
91
  (* Format.printf "%a@." Printers.pp_expr expr2;  *)
92
  (* print_path (fun fmt -> Format.fprintf fmt "(not %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
    
97 8446bf03 ploc
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =
98 3e1d20e0 ploc
  let neg_list l = 
99
    List.fold_right (fun e (vl,el) -> let vl', e' = compute_neg_expr cpt_pre e in (vl'@vl), e'::el) l ([], [])
100
  in
101 40d33d55 xavier.thirioux
  match expr.expr_desc with
102
  | Expr_tuple l -> 
103 3e1d20e0 ploc
     let vl, neg = neg_list l in
104
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
105
       
106 66359a5e ploc
  | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> (
107 40d33d55 xavier.thirioux
    let list = [i; t; e] in
108 3e1d20e0 ploc
    let vl, neg = neg_list list in
109
    vl, combine (fun l ->
110 2fdbc781 ploc
      match l with
111
      | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
112
      | _ -> assert false
113
    ) neg list
114
  )
115 40d33d55 xavier.thirioux
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
116 3e1d20e0 ploc
    let vl = gen_mcdc_cond_guard i in
117 40d33d55 xavier.thirioux
    let list = [i; t; e] in
118 3e1d20e0 ploc
    let vl', neg = neg_list list in
119
    vl@vl', combine (fun l ->
120 2fdbc781 ploc
      match l with
121
      | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
122
      | _ -> assert false
123
    ) neg list
124 40d33d55 xavier.thirioux
  )
125
  | Expr_arrow (e1, e2) -> 
126 3e1d20e0 ploc
     let vl1, e1' = compute_neg_expr cpt_pre e1 in
127
     let vl2, e2' = compute_neg_expr cpt_pre e2 in
128
     vl1@vl2, combine (fun l -> match l with
129
     | [x;y] -> { expr with expr_desc = Expr_arrow (x, y) }
130
     | _ -> assert false
131
     ) [e1'; e2'] [e1; e2]
132
133
  | Expr_pre e ->
134
     let vl, e' = compute_neg_expr (cpt_pre+1) e in
135
     vl, List.map
136
       (fun (v, negv) -> (v, { expr with expr_desc = Expr_pre negv } )) e'
137 40d33d55 xavier.thirioux
138
  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 
139 3e1d20e0 ploc
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
140 40d33d55 xavier.thirioux
141 3e1d20e0 ploc
  | Expr_appl (op_name, args, r) ->
142
     let vl, args' = compute_neg_expr cpt_pre args in
143
     vl, List.map 
144
       (fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
145
       args'
146 40d33d55 xavier.thirioux
147 66359a5e ploc
  | Expr_ident _ when (Types.is_bool_type expr.expr_type) ->
148 3e1d20e0 ploc
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
149
  | _ -> [] (* empty vars *) , [] 
150
and gen_mcdc_cond_var v expr =
151
  report ~level:1 (fun fmt ->
152
    Format.fprintf fmt ".. Generating MC/DC cond for boolean flow %s and expression %a@."
153
      v
154
      Printers.pp_expr expr);
155
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
156 ff6ba54e ploc
  if List.length leafs_n_neg_expr >= 1 then (
157 3e1d20e0 ploc
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
158
      (mcdc_var  (mk_pre nb_pre vi) expr expr_neg_vi)::accu
159
    ) vl leafs_n_neg_expr
160 40d33d55 xavier.thirioux
  )
161 ff6ba54e ploc
  else
162
    (* TODO: deal with the case length xxx = 1 with a simpler condition  *)
163
    vl
164 40d33d55 xavier.thirioux
165
and gen_mcdc_cond_guard expr =
166 3e1d20e0 ploc
  report ~level:1 (fun fmt ->
167
    Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
168
      Printers.pp_expr expr);
169
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
170 ff6ba54e ploc
  if List.length leafs_n_neg_expr >= 1 then (
171 3e1d20e0 ploc
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
172
      (mcdc_var  (mk_pre nb_pre vi) expr expr_neg_vi)::accu
173
    ) vl leafs_n_neg_expr)
174
  else
175 ff6ba54e ploc
    (* TODO: deal with the case length xxx = 1 with a simpler condition  *)
176 3e1d20e0 ploc
    vl
177 40d33d55 xavier.thirioux
  
178
179
let rec mcdc_expr cpt_pre expr = 
180
  match expr.expr_desc with
181 3e1d20e0 ploc
  | Expr_tuple l ->
182
     let vl =
183
       List.fold_right (fun e accu_v ->
184
	 let vl = mcdc_expr cpt_pre e in
185
	 (vl@accu_v))
186
	 l
187
	 []
188
     in
189
     vl
190
  | Expr_ite (i,t,e) ->
191
     let vl_i = gen_mcdc_cond_guard i in
192
     let vl_t = mcdc_expr cpt_pre t in
193
     let vl_e = mcdc_expr cpt_pre e in
194
     vl_i@vl_t@vl_e
195
  | Expr_arrow (e1, e2) ->
196
     let vl1 = mcdc_expr cpt_pre e1 in
197
     let vl2 = mcdc_expr cpt_pre e2 in
198
     vl1@vl2
199
  | Expr_pre e ->
200
     let vl = mcdc_expr (cpt_pre+1) e in
201
     vl
202
  | Expr_appl (f, args, r) ->
203
     let vl = mcdc_expr cpt_pre args in
204
     vl
205
  | _ -> []
206 40d33d55 xavier.thirioux
207
let mcdc_var_def v expr = 
208 66359a5e ploc
  if Types.is_bool_type expr.expr_type then
209 3e1d20e0 ploc
     let vl = gen_mcdc_cond_var v expr in
210
     vl
211 66359a5e ploc
  else
212
    let vl = mcdc_expr 0 expr in
213
    vl
214
      
215 40d33d55 xavier.thirioux
let mcdc_node_eq eq =
216 3e1d20e0 ploc
  let vl =
217 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
218 8cacf677 ploc
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
219 66359a5e ploc
    | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
220 3e1d20e0 ploc
       (* We iterate trough pairs, but accumulate variables aside. The resulting
221
	  expression shall remain a tuple defintion *)
222
       let vl = List.fold_right2 (fun lhs rhs accu ->
223
	 let v = mcdc_var_def lhs rhs in
224
	 (* we don't care about the expression it. We focus on the coverage
225
	    expressions in v *)
226
	 v@accu
227
       ) eq.eq_lhs rhs []
228
       in
229
       vl
230
    | _ -> mcdc_expr 0 eq.eq_rhs 
231
  in
232
  vl
233 40d33d55 xavier.thirioux
234 bde99c3f xavier.thirioux
let mcdc_node_stmt stmt =
235
  match stmt with
236 3e1d20e0 ploc
  | Eq eq -> let vl = mcdc_node_eq eq in vl
237 bde99c3f xavier.thirioux
  | Aut aut -> assert false
238
239 40d33d55 xavier.thirioux
let mcdc_top_decl td = 
240
  match td.top_decl_desc with
241 3e1d20e0 ploc
  | Node nd ->
242
     let new_coverage_exprs =
243
       List.fold_right (
244 8cacf677 ploc
	   fun s accu_v ->
245 3e1d20e0 ploc
	   let vl' = mcdc_node_stmt s in
246
	   vl'@accu_v
247 8cacf677 ploc
	 ) nd.node_stmts []
248 3e1d20e0 ploc
     in
249 8cacf677 ploc
     (* We add coverage vars as boolean internal flows. *)
250
     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
251 3e1d20e0 ploc
     let nb_total = List.length fresh_cov_defs in
252 8cacf677 ploc
     let fresh_cov_vars = List.mapi (fun i (atom, atom_valid, cov_expr) ->
253
				     let loc = cov_expr.expr_loc in
254
				     Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
255
				     let cov_id = Format.flush_str_formatter () in
256
				     let cov_var = mkvar_decl loc
257
							      (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in
258
				     let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
259
				     cov_var, cov_def, atom, atom_valid
260
				    ) fresh_cov_defs
261 3e1d20e0 ploc
     in
262 66359a5e ploc
     let fresh_vars, fresh_eqs =
263
       List.fold_right
264 8cacf677 ploc
	 (fun (v,eq,_,_) (accuv, accueq)-> v::accuv, eq::accueq )
265 66359a5e ploc
	 fresh_cov_vars
266
	 ([], [])
267
     in
268
     let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for
269
			   kind2, and regular ones to keep track of the nature
270
			   of the annotations. *)
271 3e1d20e0 ploc
       List.map
272 8cacf677 ploc
	 (fun (v, _, atom, atom_valid) ->
273
	  let e = expr_of_vdecl v in
274
	  let neg_ee = expr_to_eexpr (mkpredef_call e.expr_loc "not" [e]) in
275
	  {annots =  [["PROPERTY"], neg_ee; (* Using negated property to force
276
                                               model-checker to produce a
277
                                               suitable covering trace *)
278 c95a441d ploc
                      let loc = Location.dummy_loc in
279
		      let valid_e = let open Corelang in mkexpr loc (Expr_const (const_of_bool atom_valid)) in
280
		      ["coverage";"mcdc";v.var_id], expr_to_eexpr (Corelang.expr_of_expr_list loc [e; atom; valid_e])
281 8cacf677 ploc
		     ];
282
	   annot_loc = v.var_loc})
283
	 fresh_cov_vars
284 66359a5e ploc
     in
285
     Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;
286 3e1d20e0 ploc
     (* And add them as annotations --%PROPERTY: var TODO *)
287
     {td with top_decl_desc = Node {nd with
288 8cacf677 ploc
				     node_locals = nd.node_locals@fresh_vars;
289
				     node_stmts = nd.node_stmts@fresh_eqs;
290
				     node_annot = nd.node_annot@fresh_annots
291
				   }}
292 3e1d20e0 ploc
  | _ -> td
293 40d33d55 xavier.thirioux
294
295
let mcdc prog =
296
  (* If main node is provided add silly constraints to show in/out variables in the path condition *)
297
  if !Options.main_node <> "" then (
298
    inout_vars := 
299
      let top = List.find 
300
	(fun td -> 
301
	  match td.top_decl_desc with 
302
	  | Node nd when nd.node_id = !Options.main_node -> true
303
	  | _ -> false) 
304
	prog 
305
      in
306
      match top.top_decl_desc with
307
      | Node nd -> nd.node_inputs @ nd.node_outputs
308
      | _ -> assert false);
309 3e1d20e0 ploc
  List.map mcdc_top_decl prog
310 40d33d55 xavier.thirioux
311 66359a5e ploc
312
    
313 40d33d55 xavier.thirioux
(* Local Variables: *)
314
(* compile-command:"make -C .." *)
315
(* End: *)
316
317