Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ 8cacf677

History | View | Annotate | Download (11.4 KB)

1
open Lustre_types 
2
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
(* 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

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

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

    
26
(* 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
(*
40
   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
*)
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

    
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
  ((expr,vi_as_expr),[(true,expr1);(false,expr2)]) (* expr1 corresponds to atom
82
                                                     true while expr2
83
                                                     corresponds to atom
84
                                                     false *)
85

    
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
let rec compute_neg_expr cpt_pre (expr: Lustre_types.expr) =
98
  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
  match expr.expr_desc with
102
  | Expr_tuple l -> 
103
     let vl, neg = neg_list l in
104
     vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
105
       
106
  | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> (
107
    let list = [i; t; e] in
108
    let vl, neg = neg_list list in
109
    vl, combine (fun l ->
110
      match l with
111
      | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
112
      | _ -> assert false
113
    ) neg list
114
  )
115
  | Expr_ite (i,t,e) -> ( (* We return the guard as a new guard *)
116
    let vl = gen_mcdc_cond_guard i in
117
    let list = [i; t; e] in
118
    let vl', neg = neg_list list in
119
    vl@vl', combine (fun l ->
120
      match l with
121
      | [i'; t'; e'] -> {expr with expr_desc = Expr_ite(i', t', e')}
122
      | _ -> assert false
123
    ) neg list
124
  )
125
  | Expr_arrow (e1, e2) -> 
126
     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

    
138
  | Expr_appl (op_name, args, r) when List.mem op_name rel_op -> 
139
     [], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
140

    
141
  | 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

    
147
  | Expr_ident _ when (Types.is_bool_type expr.expr_type) ->
148
     [], [(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
  if List.length leafs_n_neg_expr > 1 then (
157
    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
  )
161
  else vl
162

    
163
and gen_mcdc_cond_guard expr =
164
  report ~level:1 (fun fmt ->
165
    Format.fprintf fmt".. Generating MC/DC cond for guard %a@."
166
      Printers.pp_expr expr);
167
  let vl, leafs_n_neg_expr = compute_neg_expr 0 expr in
168
  if List.length leafs_n_neg_expr > 1 then (
169
    List.fold_left (fun accu ((vi, nb_pre), expr_neg_vi) ->
170
      (mcdc_var  (mk_pre nb_pre vi) expr expr_neg_vi)::accu
171
    ) vl leafs_n_neg_expr)
172
  else
173
    vl
174
  
175

    
176
let rec mcdc_expr cpt_pre expr = 
177
  match expr.expr_desc with
178
  | Expr_tuple l ->
179
     let vl =
180
       List.fold_right (fun e accu_v ->
181
	 let vl = mcdc_expr cpt_pre e in
182
	 (vl@accu_v))
183
	 l
184
	 []
185
     in
186
     vl
187
  | Expr_ite (i,t,e) ->
188
     let vl_i = gen_mcdc_cond_guard i in
189
     let vl_t = mcdc_expr cpt_pre t in
190
     let vl_e = mcdc_expr cpt_pre e in
191
     vl_i@vl_t@vl_e
192
  | Expr_arrow (e1, e2) ->
193
     let vl1 = mcdc_expr cpt_pre e1 in
194
     let vl2 = mcdc_expr cpt_pre e2 in
195
     vl1@vl2
196
  | Expr_pre e ->
197
     let vl = mcdc_expr (cpt_pre+1) e in
198
     vl
199
  | Expr_appl (f, args, r) ->
200
     let vl = mcdc_expr cpt_pre args in
201
     vl
202
  | _ -> []
203

    
204
let mcdc_var_def v expr = 
205
  if Types.is_bool_type expr.expr_type then
206
     let vl = gen_mcdc_cond_var v expr in
207
     vl
208
  else
209
    let vl = mcdc_expr 0 expr in
210
    vl
211
      
212
let mcdc_node_eq eq =
213
  let vl =
214
    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
215
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
216
    | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
217
       (* We iterate trough pairs, but accumulate variables aside. The resulting
218
	  expression shall remain a tuple defintion *)
219
       let vl = List.fold_right2 (fun lhs rhs accu ->
220
	 let v = mcdc_var_def lhs rhs in
221
	 (* we don't care about the expression it. We focus on the coverage
222
	    expressions in v *)
223
	 v@accu
224
       ) eq.eq_lhs rhs []
225
       in
226
       vl
227
    | _ -> mcdc_expr 0 eq.eq_rhs 
228
  in
229
  vl
230

    
231
let mcdc_node_stmt stmt =
232
  match stmt with
233
  | Eq eq -> let vl = mcdc_node_eq eq in vl
234
  | Aut aut -> assert false
235

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

    
293

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

    
310

    
311
    
312
(* Local Variables: *)
313
(* compile-command:"make -C .." *)
314
(* End: *)
315

    
316