Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / pathConditions.ml @ master

History | View | Annotate | Download (11.5 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
162
    (* TODO: deal with the case length xxx = 1 with a simpler condition  *)
163
    vl
164

    
165
and gen_mcdc_cond_guard expr =
166
  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
  if List.length leafs_n_neg_expr >= 1 then (
171
    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
    (* TODO: deal with the case length xxx = 1 with a simpler condition  *)
176
    vl
177
  
178

    
179
let rec mcdc_expr cpt_pre expr = 
180
  match expr.expr_desc with
181
  | 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

    
207
let mcdc_var_def v expr = 
208
  if Types.is_bool_type expr.expr_type then
209
     let vl = gen_mcdc_cond_var v expr in
210
     vl
211
  else
212
    let vl = mcdc_expr 0 expr in
213
    vl
214
      
215
let mcdc_node_eq eq =
216
  let vl =
217
    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
    | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs 
219
    | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
220
       (* 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

    
234
let mcdc_node_stmt stmt =
235
  match stmt with
236
  | Eq eq -> let vl = mcdc_node_eq eq in vl
237
  | Aut aut -> assert false
238

    
239
let mcdc_top_decl td = 
240
  match td.top_decl_desc with
241
  | Node nd ->
242
     let new_coverage_exprs =
243
       List.fold_right (
244
	   fun s accu_v ->
245
	   let vl' = mcdc_node_stmt s in
246
	   vl'@accu_v
247
	 ) nd.node_stmts []
248
     in
249
     (* 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
     let nb_total = List.length fresh_cov_defs in
252
     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
     in
262
     let fresh_vars, fresh_eqs =
263
       List.fold_right
264
	 (fun (v,eq,_,_) (accuv, accueq)-> v::accuv, eq::accueq )
265
	 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
       List.map
272
	 (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
                      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
		     ];
282
	   annot_loc = v.var_loc})
283
	 fresh_cov_vars
284
     in
285
     Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;
286
     (* And add them as annotations --%PROPERTY: var TODO *)
287
     {td with top_decl_desc = Node {nd with
288
				     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
  | _ -> td
293

    
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
  List.map mcdc_top_decl prog
310

    
311

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

    
317